Commit 2022-12-24 09:17 d1bcc450

View on Github →

feat: port Data.Set.Intervals.OrdConnected (#1186)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Set/Intervals/OrdConnected.lean

added theorem Set.OrdConnected.dual

added theorem Set.OrdConnected.inter

added theorem Set.OrdConnected.interval_oc_subset

added theorem Set.OrdConnected.interval_subset

added theorem Set.OrdConnected.out

added theorem Set.OrdConnected.preimage_anti

added theorem Set.OrdConnected.preimage_mono

added theorem Set.OrdConnected_Icc

added theorem Set.OrdConnected_Ici

added theorem Set.OrdConnected_Ico

added theorem Set.OrdConnected_Iic

added theorem Set.OrdConnected_Iio

added theorem Set.OrdConnected_Ioc

added theorem Set.OrdConnected_Ioi

added theorem Set.OrdConnected_Ioo

added theorem Set.OrdConnected_binterᵢ

added theorem Set.OrdConnected_def

added theorem Set.OrdConnected_dual

added theorem Set.OrdConnected_empty

added theorem Set.OrdConnected_iff

added theorem Set.OrdConnected_iff_interval_subset

added theorem Set.OrdConnected_iff_interval_subset_left

added theorem Set.OrdConnected_iff_interval_subset_right

added theorem Set.OrdConnected_image

added theorem Set.OrdConnected_interval

added theorem Set.OrdConnected_interval_oc

added theorem Set.OrdConnected_interᵢ

added theorem Set.OrdConnected_interₛ

added theorem Set.OrdConnected_of_Ioo

added theorem Set.OrdConnected_of_interval_subset_left

added theorem Set.OrdConnected_pi

added theorem Set.OrdConnected_preimage

added theorem Set.OrdConnected_range

added theorem Set.OrdConnected_singleton

added theorem Set.OrdConnected_univ

added theorem Set.dual_OrdConnected

added theorem Set.dual_OrdConnected_iff