mathlib documentation

analysis.​calculus.​lhopital

analysis.​calculus.​lhopital

source
deriv.​lhopital_zero_at_bot
deriv.​lhopital_zero_at_bot_on_Iio
deriv.​lhopital_zero_at_top
deriv.​lhopital_zero_at_top_on_Ioi
deriv.​lhopital_zero_left_on_Ioo
deriv.​lhopital_zero_nhds
deriv.​lhopital_zero_nhds'
deriv.​lhopital_zero_nhds_left
deriv.​lhopital_zero_nhds_right
deriv.​lhopital_zero_right_on_Ico
deriv.​lhopital_zero_right_on_Ioo
has_deriv_at.​lhopital_zero_at_bot
has_deriv_at.​lhopital_zero_at_bot_on_Iio
has_deriv_at.​lhopital_zero_at_top
has_deriv_at.​lhopital_zero_at_top_on_Ioi
has_deriv_at.​lhopital_zero_left_on_Ioc
has_deriv_at.​lhopital_zero_left_on_Ioo
has_deriv_at.​lhopital_zero_nhds
has_deriv_at.​lhopital_zero_nhds'
has_deriv_at.​lhopital_zero_nhds_left
has_deriv_at.​lhopital_zero_nhds_right
has_deriv_at.​lhopital_zero_right_on_Ico
has_deriv_at.​lhopital_zero_right_on_Ioo

L'HΓ΄pital's rule for 0/0 indeterminate forms

In this file, we prove several forms of "L'Hopital's rule" for computing 0/0 indeterminate forms. The proof of has_deriv_at.lhopital_zero_right_on_Ioo is based on the one given in the corresponding Wikibooks chapter, and all other statements are derived from this one by composing by carefully chosen functions.

Note that the filter f'/g' tends to isn't required to be one of 𝓝 a, at_top or at_bot. In fact, we give a slightly stronger statement by allowing it to be any filter on ℝ.

Each statement is available in a has_deriv_at form and a deriv form, which is denoted by each statement being in either the has_deriv_at or the deriv namespace.

Interval-based versions

We start by proving statements where all conditions (derivability, g' β‰  0) have to be satisfied on an explicitely-provided interval.

source
theorem has_deriv_at.​lhopital_zero_right_on_Ioo {a b : ℝ} (hab : a < b) {l : filter ℝ} {f f' g g' : ℝ β†’ ℝ} :
(βˆ€ (x : ℝ), x ∈ set.Ioo a b β†’ has_deriv_at f (f' x) x) β†’ (βˆ€ (x : ℝ), x ∈ set.Ioo a b β†’ has_deriv_at g (g' x) x) β†’ (βˆ€ (x : ℝ), x ∈ set.Ioo a b β†’ g' x β‰  0) β†’ filter.tendsto f (nhds_within a (set.Ioi a)) (nhds 0) β†’ filter.tendsto g (nhds_within a (set.Ioi a)) (nhds 0) β†’ filter.tendsto (Ξ» (x : ℝ), f' x / g' x) (nhds_within a (set.Ioi a)) l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) (nhds_within a (set.Ioi a)) l

source
theorem has_deriv_at.​lhopital_zero_right_on_Ico {a b : ℝ} (hab : a < b) {l : filter ℝ} {f f' g g' : ℝ β†’ ℝ} :
(βˆ€ (x : ℝ), x ∈ set.Ioo a b β†’ has_deriv_at f (f' x) x) β†’ (βˆ€ (x : ℝ), x ∈ set.Ioo a b β†’ has_deriv_at g (g' x) x) β†’ continuous_on f (set.Ico a b) β†’ continuous_on g (set.Ico a b) β†’ (βˆ€ (x : ℝ), x ∈ set.Ioo a b β†’ g' x β‰  0) β†’ f a = 0 β†’ g a = 0 β†’ filter.tendsto (Ξ» (x : ℝ), f' x / g' x) (nhds_within a (set.Ioi a)) l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) (nhds_within a (set.Ioi a)) l

source
theorem has_deriv_at.​lhopital_zero_left_on_Ioo {a b : ℝ} (hab : a < b) {l : filter ℝ} {f f' g g' : ℝ β†’ ℝ} :
(βˆ€ (x : ℝ), x ∈ set.Ioo a b β†’ has_deriv_at f (f' x) x) β†’ (βˆ€ (x : ℝ), x ∈ set.Ioo a b β†’ has_deriv_at g (g' x) x) β†’ (βˆ€ (x : ℝ), x ∈ set.Ioo a b β†’ g' x β‰  0) β†’ filter.tendsto f (nhds_within b (set.Iio b)) (nhds 0) β†’ filter.tendsto g (nhds_within b (set.Iio b)) (nhds 0) β†’ filter.tendsto (Ξ» (x : ℝ), f' x / g' x) (nhds_within b (set.Iio b)) l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) (nhds_within b (set.Iio b)) l

source
theorem has_deriv_at.​lhopital_zero_left_on_Ioc {a b : ℝ} (hab : a < b) {l : filter ℝ} {f f' g g' : ℝ β†’ ℝ} :
(βˆ€ (x : ℝ), x ∈ set.Ioo a b β†’ has_deriv_at f (f' x) x) β†’ (βˆ€ (x : ℝ), x ∈ set.Ioo a b β†’ has_deriv_at g (g' x) x) β†’ continuous_on f (set.Ioc a b) β†’ continuous_on g (set.Ioc a b) β†’ (βˆ€ (x : ℝ), x ∈ set.Ioo a b β†’ g' x β‰  0) β†’ f b = 0 β†’ g b = 0 β†’ filter.tendsto (Ξ» (x : ℝ), f' x / g' x) (nhds_within b (set.Iio b)) l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) (nhds_within b (set.Iio b)) l

source
theorem has_deriv_at.​lhopital_zero_at_top_on_Ioi {a : ℝ} {l : filter ℝ} {f f' g g' : ℝ β†’ ℝ} :
(βˆ€ (x : ℝ), x ∈ set.Ioi a β†’ has_deriv_at f (f' x) x) β†’ (βˆ€ (x : ℝ), x ∈ set.Ioi a β†’ has_deriv_at g (g' x) x) β†’ (βˆ€ (x : ℝ), x ∈ set.Ioi a β†’ g' x β‰  0) β†’ filter.tendsto f filter.at_top (nhds 0) β†’ filter.tendsto g filter.at_top (nhds 0) β†’ filter.tendsto (Ξ» (x : ℝ), f' x / g' x) filter.at_top l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) filter.at_top l

source
theorem has_deriv_at.​lhopital_zero_at_bot_on_Iio {a : ℝ} {l : filter ℝ} {f f' g g' : ℝ β†’ ℝ} :
(βˆ€ (x : ℝ), x ∈ set.Iio a β†’ has_deriv_at f (f' x) x) β†’ (βˆ€ (x : ℝ), x ∈ set.Iio a β†’ has_deriv_at g (g' x) x) β†’ (βˆ€ (x : ℝ), x ∈ set.Iio a β†’ g' x β‰  0) β†’ filter.tendsto f filter.at_bot (nhds 0) β†’ filter.tendsto g filter.at_bot (nhds 0) β†’ filter.tendsto (Ξ» (x : ℝ), f' x / g' x) filter.at_bot l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) filter.at_bot l

source
theorem deriv.​lhopital_zero_right_on_Ioo {a b : ℝ} (hab : a < b) {l : filter ℝ} {f g : ℝ β†’ ℝ} :
differentiable_on ℝ f (set.Ioo a b) β†’ (βˆ€ (x : ℝ), x ∈ set.Ioo a b β†’ deriv g x β‰  0) β†’ filter.tendsto f (nhds_within a (set.Ioi a)) (nhds 0) β†’ filter.tendsto g (nhds_within a (set.Ioi a)) (nhds 0) β†’ filter.tendsto (Ξ» (x : ℝ), deriv f x / deriv g x) (nhds_within a (set.Ioi a)) l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) (nhds_within a (set.Ioi a)) l

source
theorem deriv.​lhopital_zero_right_on_Ico {a b : ℝ} (hab : a < b) {l : filter ℝ} {f g : ℝ β†’ ℝ} :
differentiable_on ℝ f (set.Ioo a b) β†’ continuous_on f (set.Ico a b) β†’ continuous_on g (set.Ico a b) β†’ (βˆ€ (x : ℝ), x ∈ set.Ioo a b β†’ deriv g x β‰  0) β†’ f a = 0 β†’ g a = 0 β†’ filter.tendsto (Ξ» (x : ℝ), deriv f x / deriv g x) (nhds_within a (set.Ioi a)) l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) (nhds_within a (set.Ioi a)) l

source
theorem deriv.​lhopital_zero_left_on_Ioo {a b : ℝ} (hab : a < b) {l : filter ℝ} {f g : ℝ β†’ ℝ} :
differentiable_on ℝ f (set.Ioo a b) β†’ (βˆ€ (x : ℝ), x ∈ set.Ioo a b β†’ deriv g x β‰  0) β†’ filter.tendsto f (nhds_within b (set.Iio b)) (nhds 0) β†’ filter.tendsto g (nhds_within b (set.Iio b)) (nhds 0) β†’ filter.tendsto (Ξ» (x : ℝ), deriv f x / deriv g x) (nhds_within b (set.Iio b)) l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) (nhds_within b (set.Iio b)) l

source
theorem deriv.​lhopital_zero_at_top_on_Ioi {a : ℝ} {l : filter ℝ} {f g : ℝ β†’ ℝ} :
differentiable_on ℝ f (set.Ioi a) β†’ (βˆ€ (x : ℝ), x ∈ set.Ioi a β†’ deriv g x β‰  0) β†’ filter.tendsto f filter.at_top (nhds 0) β†’ filter.tendsto g filter.at_top (nhds 0) β†’ filter.tendsto (Ξ» (x : ℝ), deriv f x / deriv g x) filter.at_top l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) filter.at_top l

source
theorem deriv.​lhopital_zero_at_bot_on_Iio {a : ℝ} {l : filter ℝ} {f g : ℝ β†’ ℝ} :
differentiable_on ℝ f (set.Iio a) β†’ (βˆ€ (x : ℝ), x ∈ set.Iio a β†’ deriv g x β‰  0) β†’ filter.tendsto f filter.at_bot (nhds 0) β†’ filter.tendsto g filter.at_bot (nhds 0) β†’ filter.tendsto (Ξ» (x : ℝ), deriv f x / deriv g x) filter.at_bot l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) filter.at_bot l

Generic versions

The following statements no longer any explicit interval, as they only require conditions holding eventually.

source
theorem has_deriv_at.​lhopital_zero_nhds_right {a : ℝ} {l : filter ℝ} {f f' g g' : ℝ β†’ ℝ} :
(βˆ€αΆ  (x : ℝ) in nhds_within a (set.Ioi a), has_deriv_at f (f' x) x) β†’ (βˆ€αΆ  (x : ℝ) in nhds_within a (set.Ioi a), has_deriv_at g (g' x) x) β†’ (βˆ€αΆ  (x : ℝ) in nhds_within a (set.Ioi a), g' x β‰  0) β†’ filter.tendsto f (nhds_within a (set.Ioi a)) (nhds 0) β†’ filter.tendsto g (nhds_within a (set.Ioi a)) (nhds 0) β†’ filter.tendsto (Ξ» (x : ℝ), f' x / g' x) (nhds_within a (set.Ioi a)) l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) (nhds_within a (set.Ioi a)) l

L'HΓ΄pital's rule for approaching a real from the right, has_deriv_at version

source
theorem has_deriv_at.​lhopital_zero_nhds_left {a : ℝ} {l : filter ℝ} {f f' g g' : ℝ β†’ ℝ} :
(βˆ€αΆ  (x : ℝ) in nhds_within a (set.Iio a), has_deriv_at f (f' x) x) β†’ (βˆ€αΆ  (x : ℝ) in nhds_within a (set.Iio a), has_deriv_at g (g' x) x) β†’ (βˆ€αΆ  (x : ℝ) in nhds_within a (set.Iio a), g' x β‰  0) β†’ filter.tendsto f (nhds_within a (set.Iio a)) (nhds 0) β†’ filter.tendsto g (nhds_within a (set.Iio a)) (nhds 0) β†’ filter.tendsto (Ξ» (x : ℝ), f' x / g' x) (nhds_within a (set.Iio a)) l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) (nhds_within a (set.Iio a)) l

L'HΓ΄pital's rule for approaching a real from the left, has_deriv_at version

source
theorem has_deriv_at.​lhopital_zero_nhds' {a : ℝ} {l : filter ℝ} {f f' g g' : ℝ β†’ ℝ} :
(βˆ€αΆ  (x : ℝ) in nhds_within a (set.univ \ {a}), has_deriv_at f (f' x) x) β†’ (βˆ€αΆ  (x : ℝ) in nhds_within a (set.univ \ {a}), has_deriv_at g (g' x) x) β†’ (βˆ€αΆ  (x : ℝ) in nhds_within a (set.univ \ {a}), g' x β‰  0) β†’ filter.tendsto f (nhds_within a (set.univ \ {a})) (nhds 0) β†’ filter.tendsto g (nhds_within a (set.univ \ {a})) (nhds 0) β†’ filter.tendsto (Ξ» (x : ℝ), f' x / g' x) (nhds_within a (set.univ \ {a})) l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) (nhds_within a (set.univ \ {a})) l

L'HΓ΄pital's rule for approaching a real, has_deriv_at version. This does not require anything about the situation at a

source
theorem has_deriv_at.​lhopital_zero_nhds {a : ℝ} {l : filter ℝ} {f f' g g' : ℝ β†’ ℝ} :
(βˆ€αΆ  (x : ℝ) in nhds a, has_deriv_at f (f' x) x) β†’ (βˆ€αΆ  (x : ℝ) in nhds a, has_deriv_at g (g' x) x) β†’ (βˆ€αΆ  (x : ℝ) in nhds a, g' x β‰  0) β†’ filter.tendsto f (nhds a) (nhds 0) β†’ filter.tendsto g (nhds a) (nhds 0) β†’ filter.tendsto (Ξ» (x : ℝ), f' x / g' x) (nhds a) l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) (nhds_within a (set.univ \ {a})) l

L'HΓ΄pital's rule for approaching a real, has_deriv_at version

source
theorem has_deriv_at.​lhopital_zero_at_top {l : filter ℝ} {f f' g g' : ℝ β†’ ℝ} :
(βˆ€αΆ  (x : ℝ) in filter.at_top, has_deriv_at f (f' x) x) β†’ (βˆ€αΆ  (x : ℝ) in filter.at_top, has_deriv_at g (g' x) x) β†’ (βˆ€αΆ  (x : ℝ) in filter.at_top, g' x β‰  0) β†’ filter.tendsto f filter.at_top (nhds 0) β†’ filter.tendsto g filter.at_top (nhds 0) β†’ filter.tendsto (Ξ» (x : ℝ), f' x / g' x) filter.at_top l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) filter.at_top l

L'Hôpital's rule for approaching +∞, has_deriv_at version

source
theorem has_deriv_at.​lhopital_zero_at_bot {l : filter ℝ} {f f' g g' : ℝ β†’ ℝ} :
(βˆ€αΆ  (x : ℝ) in filter.at_bot, has_deriv_at f (f' x) x) β†’ (βˆ€αΆ  (x : ℝ) in filter.at_bot, has_deriv_at g (g' x) x) β†’ (βˆ€αΆ  (x : ℝ) in filter.at_bot, g' x β‰  0) β†’ filter.tendsto f filter.at_bot (nhds 0) β†’ filter.tendsto g filter.at_bot (nhds 0) β†’ filter.tendsto (Ξ» (x : ℝ), f' x / g' x) filter.at_bot l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) filter.at_bot l

L'Hôpital's rule for approaching -∞, has_deriv_at version

source
theorem deriv.​lhopital_zero_nhds_right {a : ℝ} {l : filter ℝ} {f g : ℝ β†’ ℝ} :
(βˆ€αΆ  (x : ℝ) in nhds_within a (set.Ioi a), differentiable_at ℝ f x) β†’ (βˆ€αΆ  (x : ℝ) in nhds_within a (set.Ioi a), deriv g x β‰  0) β†’ filter.tendsto f (nhds_within a (set.Ioi a)) (nhds 0) β†’ filter.tendsto g (nhds_within a (set.Ioi a)) (nhds 0) β†’ filter.tendsto (Ξ» (x : ℝ), deriv f x / deriv g x) (nhds_within a (set.Ioi a)) l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) (nhds_within a (set.Ioi a)) l

L'HΓ΄pital's rule for approaching a real from the right, deriv version

source
theorem deriv.​lhopital_zero_nhds_left {a : ℝ} {l : filter ℝ} {f g : ℝ β†’ ℝ} :
(βˆ€αΆ  (x : ℝ) in nhds_within a (set.Iio a), differentiable_at ℝ f x) β†’ (βˆ€αΆ  (x : ℝ) in nhds_within a (set.Iio a), deriv g x β‰  0) β†’ filter.tendsto f (nhds_within a (set.Iio a)) (nhds 0) β†’ filter.tendsto g (nhds_within a (set.Iio a)) (nhds 0) β†’ filter.tendsto (Ξ» (x : ℝ), deriv f x / deriv g x) (nhds_within a (set.Iio a)) l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) (nhds_within a (set.Iio a)) l

L'HΓ΄pital's rule for approaching a real from the left, deriv version

source
theorem deriv.​lhopital_zero_nhds' {a : ℝ} {l : filter ℝ} {f g : ℝ β†’ ℝ} :
(βˆ€αΆ  (x : ℝ) in nhds_within a (set.univ \ {a}), differentiable_at ℝ f x) β†’ (βˆ€αΆ  (x : ℝ) in nhds_within a (set.univ \ {a}), deriv g x β‰  0) β†’ filter.tendsto f (nhds_within a (set.univ \ {a})) (nhds 0) β†’ filter.tendsto g (nhds_within a (set.univ \ {a})) (nhds 0) β†’ filter.tendsto (Ξ» (x : ℝ), deriv f x / deriv g x) (nhds_within a (set.univ \ {a})) l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) (nhds_within a (set.univ \ {a})) l

L'HΓ΄pital's rule for approaching a real, deriv version. This does not require anything about the situation at a

source
theorem deriv.​lhopital_zero_nhds {a : ℝ} {l : filter ℝ} {f g : ℝ β†’ ℝ} :
(βˆ€αΆ  (x : ℝ) in nhds a, differentiable_at ℝ f x) β†’ (βˆ€αΆ  (x : ℝ) in nhds a, deriv g x β‰  0) β†’ filter.tendsto f (nhds a) (nhds 0) β†’ filter.tendsto g (nhds a) (nhds 0) β†’ filter.tendsto (Ξ» (x : ℝ), deriv f x / deriv g x) (nhds a) l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) (nhds_within a (set.univ \ {a})) l

L'HΓ΄pital's rule for approaching a real, deriv version

source
theorem deriv.​lhopital_zero_at_top {l : filter ℝ} {f g : ℝ β†’ ℝ} :
(βˆ€αΆ  (x : ℝ) in filter.at_top, differentiable_at ℝ f x) β†’ (βˆ€αΆ  (x : ℝ) in filter.at_top, deriv g x β‰  0) β†’ filter.tendsto f filter.at_top (nhds 0) β†’ filter.tendsto g filter.at_top (nhds 0) β†’ filter.tendsto (Ξ» (x : ℝ), deriv f x / deriv g x) filter.at_top l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) filter.at_top l

L'Hôpital's rule for approaching +∞, deriv version

source
theorem deriv.​lhopital_zero_at_bot {l : filter ℝ} {f g : ℝ β†’ ℝ} :
(βˆ€αΆ  (x : ℝ) in filter.at_bot, differentiable_at ℝ f x) β†’ (βˆ€αΆ  (x : ℝ) in filter.at_bot, deriv g x β‰  0) β†’ filter.tendsto f filter.at_bot (nhds 0) β†’ filter.tendsto g filter.at_bot (nhds 0) β†’ filter.tendsto (Ξ» (x : ℝ), deriv f x / deriv g x) filter.at_bot l β†’ filter.tendsto (Ξ» (x : ℝ), f x / g x) filter.at_bot l

L'Hôpital's rule for approaching -∞, deriv version

General documentation

index
tactics
commands
hole commands
attributes
notes

Additional documentation

mathlib overview
tactic writing
calc mode
conv mode
simplification
well founded recursion
style guide
documentation style guide
naming conventions

Library

algebra
big_operators
basic
intervals
order
pi
ring
category
Algebra
basic
limits
CommRing
adjunctions
basic
colimits
limits
Group
Z_Module_equivalence
abelian
adjunctions
basic
biproducts
colimits
images
limits
preadditive
zero
Module
abelian
basic
kernels
limits
monoidal
Mon
basic
colimits
limits
continued_fractions
computation
approximations
basic
correctness_terminating
translations
basic
continuants_recurrence
convergents_equiv
terminated_stable
translations
group
basic
commute
conj
defs
hom
inj_surj
pi
prod
semiconj
to_additive
type_tags
ulift
units
units_hom
with_one
homology
chain_complex
exact
homology
image_to_kernel_map
module
basic
ordered
pi
prod
submodule
ulift
polynomial
big_operators
ring
basic
pi
prod
ulift
add_torsor
archimedean
associated
char_p
char_zero
classical_lie_algebras
direct_limit
direct_sum
divisibility
euclidean_domain
field
field_power
floor
free
free_monoid
gcd_monoid
geom_sum
group_action_hom
group_power
group_ring_action
group_with_zero
group_with_zero_power
invertible
iterate_hom
lie_algebra
linear_ordered_comm_group_with_zero
linear_recurrence
midpoint
opposites
order
order_functions
ordered_field
ordered_group
ordered_ring
pointwise
punit_instances
quadratic_discriminant
algebraic_geometry
presheafed_space
prime_spectrum
stalks
analysis
ODE
gronwall
analytic
basic
composition
calculus
darboux
deriv
extend_deriv
fderiv
implicit
inverse
iterated_deriv
lhopital
local_extr
mean_value
specific_functions
tangent_cone
times_cont_diff
complex
basic
polynomial
convex
basic
caratheodory
cone
extrema
specific_functions
topology
normed_space
add_torsor
banach
basic
bounded_linear_maps
complemented
dual
enorm
extend
finite_dimension
hahn_banach
indicator_function
mazur_ulam
multilinear
operator_norm
point_reflection
real_inner_product
riesz_lemma
units
special_functions
arsinh
exp_log
pow
trigonometric
asymptotics
hofer
mean_inequalities
specific_limits
category_theory
abelian
diagram_lemmas
four
basic
exact
non_preadditive
pseudoelements
adjunction
basic
fully_faithful
limits
opposites
category
Cat
Groupoid
Kleisli
Rel
default
closed
cartesian
monoidal
concrete_category
basic
bundled
bundled_hom
reflects_isomorphisms
unbundled_hom
limits
preserves
basic
shapes
shapes
constructions
over
connected
default
products
binary_products
equalizers
limits_of_products_and_equalizers
preserve_binary_products
pullbacks
binary_products
biproducts
concrete_category
equalizers
finite_limits
finite_products
images
kernels
products
pullbacks
regular_mono
strong_epi
terminal
types
wide_pullbacks
zero
concrete_category
cones
connected
creates
fubini
functor_category
lattice
limits
opposites
over
pi
punit
types
monad
adjunction
algebra
basic
bundled
equiv_mon
limits
types
monoidal
internal
functor_category
types
End
braided
category
functor
functor_category
functorial
internal
of_has_finite_products
types
unitors
pi
basic
preadditive
biproducts
default
schur
products
associator
basic
bifunctor
sums
associator
basic
action
arrow
comma
conj
connected
const
core
currying
differential_object
discrete_category
elements
endomorphism
epi_mono
eq_to_hom
equivalence
full_subcategory
fully_faithful
functor
functor_category
functorial
graded_object
groupoid
hom_functor
isomorphism
isomorphism_classes
natural_isomorphism
natural_transformation
opposites
over
pempty
punit
quotient
reflects_isomorphisms
shift
simple
single_obj
sparse
types
whiskering
yoneda
combinatorics
composition
simple_graph
computability
halting
partrec
partrec_code
primrec
reduce
tm_to_partrec
turing_machine
control
bitraversable
basic
instances
lemmas
equiv_functor
instances
functor
multivariate
monad
basic
cont
writer
traversable
basic
derive
equiv
instances
lemmas
applicative
basic
bifunctor
equiv_functor
fold
functor
uliftable
core
data
buffer
parser
bitvec
buffer
dlist
lazy_list
stream
vector
init
algebra
classes
functions
order
control
alternative
applicative
combinators
except
functor
id
lawful
lift
monad
monad_fail
option
reader
state
data
array
basic
slice
bool
basic
lemmas
char
basic
classes
lemmas
fin
basic
ops
int
basic
bitwise
comp_lemmas
order
list
basic
instances
lemmas
qsort
nat
basic
bitwise
div
gcd
lemmas
option
basic
instances
ordering
basic
lemmas
rbmap
basic
rbtree
basic
default
sigma
basic
lex
string
basic
ops
subtype
basic
instances
sum
basic
unsigned
basic
ops
prod
punit
quot
repr
set
setoid
to_string
meta
converter
conv
interactive
lean
parser
smt
congruence_closure
ematch
interactive
rsimp
smt_tactic
widget
basic
html_cmd
interactive_expr
replace_save_info
tactic_component
ac_tactics
async_tactic
attribute
backward
case_tag
comp_value_tactics
congr_lemma
congr_tactic
constructor_tactic
contradiction_tactic
declaration
derive
environment
exceptional
expr
expr_address
float
format
fun_info
has_reflect
hole_command
injection_tactic
interaction_monad
interactive
interactive_base
level
local_context
match_tactic
mk_dec_eq_instance
mk_has_reflect_instance
mk_has_sizeof_instance
mk_inhabited_instance
module_info
name
occurrences
options
pexpr
rb_map
rec_util
ref
relation_tactics
rewrite_tactic
set_get_option_tactics
simp_tactic
tactic
tagged_format
task
type_context
vm
well_founded_tactics
cc_lemmas
classical
coe
core
default
function
funext
ite_simp
logic
propext
util
version
wf
system
io
io_interface
random
data
analysis
filter
topology
array
lemmas
bitvec
basic
buffer
basic
complex
basic
exponential
module
dlist
basic
instances
equiv
encodable
basic
lattice
basic
denumerable
fin
functor
list
local_equiv
mul_add
nat
ring
transfer_instance
finset
basic
fold
intervals
lattice
nat_antidiagonal
order
pi
powerset
sort
finsupp
basic
lattice
pointwise
fintype
basic
card
intervals
sort
fp
basic
int
basic
cast
char_zero
gcd
modeq
parity
range
sqrt
list
alist
bag_inter
basic
chain
defs
erase_dup
forall2
func
indexes
intervals
min_max
nat_antidiagonal
nodup
of_fn
pairwise
palindrome
perm
range
rotate
sections
sigma
sort
tfae
zip
matrix
basic
notation
pequiv
multiset
antidiagonal
basic
erase_dup
finset_ops
fold
functor
intervals
lattice
nat_antidiagonal
nodup
pi
powerset
range
sections
sort
nat
basic
cast
choose
digits
dist
enat
fib
gcd
modeq
multiplicity
pairing
parity
prime
sqrt
totient
num
basic
bitwise
lemmas
prime
option
basic
defs
padics
hensel
padic_integers
padic_norm
padic_numbers
pfunctor
multivariate
M
W
basic
univariate
M
basic
pnat
basic
factors
intervals
xgcd
polynomial
degree
basic
algebra_map
basic
coeff
degree
derivative
div
eval
field_division
identities
induction
integral_normalization
monic
monomial
ring_division
qpf
multivariate
constructions
cofix
comp
const
fix
prj
quot
sigma
basic
univariate
basic
rat
basic
cast
denumerable
floor
meta_defs
order
sqrt
real
basic
cardinality
cau_seq
cau_seq_completion
conjugate_exponents
ennreal
ereal
golden_ratio
hyperreal
irrational
nnreal
pi
seq
computation
parallel
seq
wseq
set
intervals
basic
disjoint
image_preimage
ord_connected
unordered_interval
basic
countable
disjointed
enumerate
finite
function
lattice
setoid
basic
partition
sigma
basic
stream
basic
string
basic
defs
zmod
basic
zsqrtd
basic
gaussian_int
W
bool
char
dfinsupp
erased
fin
fin2
fin_enum
finmap
hash_map
holor
indicator_function
lazy_list2
mllist
monoid_algebra
mv_polynomial
opposite
pequiv
pfun
prod
quot
rel
semiquot
subtype
sum
support
sym
sym2
tree
typevec
ulift
vector2
deprecated
group
ring
subgroup
submonoid
dynamics
circle
rotation_number
translation_number
fixed_points
basic
topology
periodic_pts
field_theory
algebraic_closure
chevalley_warning
finite
fixed
minimal_polynomial
mv_polynomial
normal
perfect_closure
separable
splitting_field
subfield
tower
geometry
algebra
lie_group
euclidean
basic
circumcenter
monge_point
triangle
manifold
basic_smooth_bundle
charted_space
local_invariant_properties
mfderiv
real_instances
smooth_manifold_with_corners
times_cont_mdiff
group_theory
perm
cycles
sign
submonoid
basic
membership
operations
abelianization
congruence
coset
eckmann_hilton
free_abelian_group
free_group
group_action
monoid_localization
order_of_element
presented_group
quotient_group
semidirect_product
subgroup
sylow
linear_algebra
affine_space
basic
combination
finite_dimensional
independent
char_poly
coeff
direct_sum
finsupp
tensor_product
adic_completion
basic
basis
bilinear_form
char_poly
contraction
determinant
dimension
direct_sum_module
dual
finite_dimensional
finsupp
finsupp_vector_space
invariant_basis_number
lagrange
linear_action
linear_pmap
matrix
multilinear
nonsingular_inverse
projection
quadratic_form
sesquilinear_form
smodeq
special_linear_group
tensor_algebra
tensor_product
logic
function
basic
conjugate
iterate
basic
embedding
nontrivial
relation
relator
unique
measure_theory
category
Meas
ae_eq_fun
bochner_integration
borel_space
content
decomposition
giry_monad
group
haar_measure
integration
interval_integral
l1_space
lebesgue_measure
measurable_space
measure_space
outer_measure
probability_mass_function
set_integral
simple_func_dense
meta
coinductive_predicates
expr
expr_lens
rb_map
uchange
number_theory
basic
bernoulli
dioph
lucas_lehmer
pell
primorial
pythagorean_triples
quadratic_reciprocity
sum_four_squares
sum_two_squares
order
category
LinearOrder
NonemptyFinLinOrd
PartialOrder
Preorder
filter
at_top_bot
bases
basic
cofinite
countable_Inter
extr
filter_product
germ
indicator_function
interval
lift
partial
pointwise
ultrafilter
basic
boolean_algebra
bounded_lattice
bounds
complete_boolean_algebra
complete_lattice
conditionally_complete_lattice
copy
directed
fixed_points
galois_connection
ideal
iterate
lattice
lexicographic
liminf_limsup
ord_continuous
order_iso_nat
pilex
rel_classes
rel_iso
semiconj_Sup
zorn
representation_theory
maschke
ring_theory
ideal
basic
operations
over
polynomial
basic
homogeneous
rational_root
valuation
basic
adjoin
adjoin_root
algebra
algebra_operations
algebra_tower
algebraic
coprime
derivation
discrete_valuation_ring
eisenstein_criterion
euclidean_domain
fintype
fractional_ideal
free_comm_ring
free_ring
integral_closure
integral_domain
jacobson
jacobson_ideal
localization
maps
matrix_algebra
multiplicity
noetherian
polynomial_algebra
power_series
prime
principal_ideal_domain
subring
subsemiring
tensor_product
unique_factorization_domain
set_theory
game
domineering
impartial
nim
short
state
winner
cardinal
cardinal_ordinal
cofinality
game
lists
ordinal
ordinal_arithmetic
ordinal_notation
pgame
schroeder_bernstein
surreal
zfc
system
random
basic
tactic
converter
apply_congr
binders
interactive
old_conv
linarith
datatypes
elimination
frontend
lemmas
parsing
preprocessing
verification
lint
basic
default
frontend
misc
simp
type_classes
monotonicity
basic
interactive
lemmas
nth_rewrite
basic
congr
default
omega
int
dnf
form
main
preterm
nat
dnf
form
main
neg_elim
preterm
sub_elim
clause
coeffs
eq_elim
find_ees
find_scalars
lin_comb
main
misc
prove_unsats
term
rewrite_all
basic
abel
algebra
alias
apply
apply_fun
auto_cases
binder_matching
cache
cancel_denoms
chain
choose
clear
core
dec_trivial
delta_instance
derive_fintype
derive_inhabited
doc_commands
elide
equiv_rw
explode
ext
fin_cases
find
find_unused
finish
fix_reflect_string
generalize_proofs
generalizes
group
hint
interactive
interactive_expr
interval_cases
lift
local_cache
localized
mk_iff_of_inductive_prop
noncomm_ring
norm_cast
norm_num
obviously
pi_instances
protected
push_neg
rcases
reassoc_axiom
rename_var
replacer
restate_axiom
rewrite
ring
ring2
ring_exp
scc
show_term
simp_command
simp_result
simp_rw
simpa
simps
slice
solve_by_elim
split_ifs
squeeze
subtype_instance
suggest
tauto
tfae
tidy
transfer
transform_decl
transport
trunc_cases
unfold_cases
where
with_local_reducibility
wlog
zify
topology
algebra
affine
continuous_functions
group
group_completion
infinite_sum
module
monoid
multilinear
open_subgroup
ordered
polynomial
ring
uniform_group
uniform_ring
category
Top
adjunctions
basic
epi_mono
limits
open_nhds
opens
TopCommRing
UniformSpace
instances
complex
ennreal
nnreal
real
real_vector_space
metric_space
antilipschitz
baire
basic
cau_seq_filter
closeds
completion
contracting
emetric_space
gluing
gromov_hausdorff
gromov_hausdorff_realized
hausdorff_distance
isometry
lipschitz
pi_Lp
premetric_space
sheaves
presheaf
presheaf_of_functions
sheaf
sheaf_of_functions
stalks
uniform_space
absolute_value
abstract_completion
basic
cauchy
compact_separated
compare_reals
complete_separated
completion
pi
separation
uniform_convergence
uniform_embedding
bases
basic
bounded_continuous_function
compact_open
compacts
constructions
continuous_map
continuous_on
dense_embedding
extend_from_subset
homeomorph
list
local_extr
local_homeomorph
maps
opens
order
path_connected
separation
sequences
stone_cech
subset_properties
tactic
topological_fiber_bundle