Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-12-17 18:02 52e18723

View on Github →

refactor(topology/algebra/ordered): prove IVT for a connected set (#1806)

refactor(topology/algebra/ordered): prove IVT for a connected set Also prove that intervals are connected, and deduce the classical IVT from this.
Rewrite the proof, move min_le_max to the root namespace
Adjust analysis/complex/exponential
Add comments/obtain
Add some docs
Add more docs
Move some proofs to a section with weaker running assumptions
Remove empty lines, fix a docstring
+1 docstring

Estimated changes

Modified src/algebra/order.lean

deleted theorem decidable.min_le_max

Modified src/algebra/order_functions.lean

added theorem min_le_max

Modified src/analysis/complex/exponential.lean

modified theorem real.exists_cos_eq_zero

modified theorem real.exists_sin_eq

Modified src/topology/algebra/ordered.lean

added theorem intermediate_value_Icc'

added theorem intermediate_value_Icc

added theorem intermediate_value_univ

added theorem is_connected.forall_Icc_subset

added theorem is_connected.intermediate_value

added theorem is_connected_Icc

added theorem is_connected_Ici

added theorem is_connected_Ico

added theorem is_connected_Iic

added theorem is_connected_Iio

added theorem is_connected_Ioc

added theorem is_connected_Ioi

added theorem is_connected_Ioo

added theorem is_connected_iff_forall_Icc_subset

Modified src/topology/instances/real.lean

deleted theorem real.intermediate_value'

deleted theorem real.intermediate_value

Modified src/topology/subset_properties.lean

added theorem is_connected.closure

added theorem is_connected.image

added theorem is_connected.union

added theorem is_connected_closed_iff

deleted theorem is_connected_closure

added theorem is_connected_of_forall

added theorem is_connected_of_forall_pair

deleted theorem is_connected_union