Commit 2023-01-05 21:39 acb5c0c1

View on Github →

feat: port Data.Set.Intervals.OrdConnectedComponent (#1303)

Estimated changes

Modified Mathlib.lean

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

added theorem Set.disjoint_left_ordSeparatingSet

added theorem Set.disjoint_ordT5Nhd

added theorem Set.disjoint_right_ordSeparatingSet

added theorem Set.dual_ordConnectedComponent

added theorem Set.dual_ordConnectedSection

added theorem Set.dual_ordSeparatingSet

added theorem Set.eq_of_mem_ordConnectedSection_of_interval_subset

added theorem Set.mem_ordConnectedComponent

added theorem Set.mem_ordConnectedComponent_comm

added theorem Set.mem_ordConnectedComponent_ord_connected_proj

added theorem Set.mem_ordConnectedComponent_trans

added theorem Set.nonempty_ordConnectedComponent

added def Set.ordConnectedComponent

added theorem Set.ordConnectedComponent_empty

added theorem Set.ordConnectedComponent_eq

added theorem Set.ordConnectedComponent_eq_empty

added theorem Set.ordConnectedComponent_inter

added theorem Set.ordConnectedComponent_ord_connected_proj

added theorem Set.ordConnectedComponent_subset

added theorem Set.ordConnectedComponent_univ

added theorem Set.ordConnectedProj_eq

added theorem Set.ordConnectedProj_mem_ordConnectedComponent

added def Set.ordConnectedSection

added theorem Set.ordConnectedSection_subset

added def Set.ordSeparatingSet

added theorem Set.ordSeparatingSet_comm

added def Set.ordT5Nhd

added theorem Set.self_mem_ordConnectedComponent

added theorem Set.subset_ordConnectedComponent