Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-30 14:58 9524dee3

View on Github →

feat(topology): real.image_Icc (#3224) The image of a segment under a real-valued continuous function is a segment.

Estimated changes

Modified src/order/complete_lattice.lean

deleted theorem has_Inf_to_nonempty

deleted theorem has_Sup_to_nonempty

Modified src/order/conditionally_complete_lattice.lean

added theorem subset_Icc_cInf_cSup

Modified src/topology/algebra/ordered.lean

added theorem compact.Inf_mem

added theorem compact.Sup_mem

added theorem compact.exists_Inf_image_eq

added theorem compact.exists_Sup_image_eq

added theorem compact.exists_is_glb

added theorem compact.exists_is_greatest

added theorem compact.exists_is_least

added theorem compact.exists_is_lub

added theorem compact.is_glb_Inf

added theorem compact.is_greatest_Sup

added theorem compact.is_least_Inf

added theorem compact.is_lub_Sup

added theorem eq_Icc_cInf_cSup_of_connected_bdd_closed

added theorem eq_Icc_of_connected_compact

modified theorem is_closed.cInf_mem

modified theorem is_closed.cSup_mem

added theorem is_connected.Icc_subset

Modified src/topology/instances/real.lean

added theorem real.image_Icc