Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-05 07:28 a130c73a

View on Github →

feat(topology/algebra/ordered): list of preconnected sets (#2943) A subset of a densely ordered conditionally complete lattice (e.g., ℝ) with order topology is preconnected if and only if it is one of the intervals.

Estimated changes

added theorem set.diff_compl
added theorem set.diff_diff_right
added theorem set.diff_inter
modified theorem set.mem_diff_singleton
added theorem set.Icc_diff_Ico_same
added theorem set.Icc_diff_Ioc_same
added theorem set.Icc_diff_Ioo_same
added theorem set.Icc_diff_both
added theorem set.Icc_diff_left
added theorem set.Icc_diff_right
added theorem set.Ici_diff_Ioi_same
added theorem set.Ici_diff_left
added theorem set.Ico_diff_Ioo_same
added theorem set.Ico_diff_left
added theorem set.Iic_diff_Iio_same
added theorem set.Iic_diff_right
added theorem set.Iio_union_right
added theorem set.Ioc_diff_Ioo_same
added theorem set.Ioc_diff_right
added theorem set.Ioi_union_left
added theorem not_bdd_above_iff'
added theorem not_bdd_above_iff
added theorem not_bdd_below_iff'
added theorem not_bdd_below_iff
modified theorem cInf_mem_closure
modified theorem cInf_mem_of_is_closed
modified theorem cSup_mem_closure
modified theorem cSup_mem_of_is_closed
modified theorem mem_closure_of_is_glb
modified theorem mem_closure_of_is_lub
modified theorem mem_of_is_glb_of_is_closed
modified theorem mem_of_is_lub_of_is_closed