Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-02 08:31 78655b6e

View on Github →

feat(data/set/intervals): define set.ord_connected (#3647) A set s : set α, [preorder α] is ord_connected if for any x y ∈ s we have [x, y] ⊆ s. For real numbers this property is equivalent to each of the properties convex s and is_preconnected s. We define it for any preorder, prove some basic properties, and migrate lemmas like convex_I?? and is_preconnected_I?? to this API.

Estimated changes

modified theorem convex_Icc
modified theorem convex_Ici
modified theorem convex_Ico
modified theorem convex_Iic
modified theorem convex_Iio
modified theorem convex_Ioc
modified theorem convex_Ioi
modified theorem convex_Ioo
added theorem convex_interval
deleted theorem convex_real_iff
modified theorem set.Icc_diff_Ico_same
modified theorem set.Icc_diff_Ioc_same
modified theorem set.Icc_diff_Ioo_same
modified theorem set.Icc_diff_both
modified theorem set.Icc_diff_left
modified theorem set.Icc_diff_right
modified theorem set.Ici_diff_Ioi_same
modified theorem set.Ici_diff_left
modified theorem set.Ico_diff_Ioo_same
modified theorem set.Ico_diff_left
modified theorem set.Iic_diff_Iio_same
modified theorem set.Iic_diff_right
modified theorem set.Iio_union_right
modified theorem set.Ioc_diff_Ioo_same
modified theorem set.Ioc_diff_right
modified theorem set.Ioi_union_left
added theorem set.ord_connected.dual
added theorem set.ord_connected_Icc
added theorem set.ord_connected_Ici
added theorem set.ord_connected_Ico
added theorem set.ord_connected_Iic
added theorem set.ord_connected_Iio
added theorem set.ord_connected_Ioc
added theorem set.ord_connected_Ioi
added theorem set.ord_connected_Ioo
added theorem set.ord_connected_dual
added theorem set.ord_connected_iff
added theorem set.ord_connected_univ
modified theorem is_preconnected_Ici
modified theorem is_preconnected_Ico
modified theorem is_preconnected_Iic
modified theorem is_preconnected_Iio
modified theorem is_preconnected_Ioc
modified theorem is_preconnected_Ioi
modified theorem is_preconnected_Ioo