Documentation

Mathlib.Order.Interval.Set.OrdConnectedComponent

Order connected components of a set #

In this file we define Set.ordConnectedComponent s x to be the set of y such that Set.uIcc x y ⊆ s and prove some basic facts about this definition. At the moment of writing, this construction is used only to prove that any linear order with order topology is a T₅ space, so we only add API needed for this lemma.

def Set.ordConnectedComponent {α : Type u_1} [LinearOrder α] (s : Set α) (x : α) :
Set α

Order-connected component of a point x in a set s. It is defined as the set of y such that Set.uIcc x y ⊆ s. Note that it is empty if and only if x ∉ s.

Equations
Instances For
    theorem Set.mem_ordConnectedComponent {α : Type u_1} [LinearOrder α] {s : Set α} {x : α} {y : α} :
    y s.ordConnectedComponent x Set.uIcc x y s
    theorem Set.dual_ordConnectedComponent {α : Type u_1} [LinearOrder α] {s : Set α} {x : α} :
    (OrderDual.ofDual ⁻¹' s).ordConnectedComponent (OrderDual.toDual x) = OrderDual.ofDual ⁻¹' s.ordConnectedComponent x
    theorem Set.ordConnectedComponent_subset {α : Type u_1} [LinearOrder α] {s : Set α} {x : α} :
    s.ordConnectedComponent x s
    theorem Set.subset_ordConnectedComponent {α : Type u_1} [LinearOrder α] {s : Set α} {x : α} {t : Set α} [h : s.OrdConnected] (hs : x s) (ht : s t) :
    s t.ordConnectedComponent x
    @[simp]
    theorem Set.self_mem_ordConnectedComponent {α : Type u_1} [LinearOrder α] {s : Set α} {x : α} :
    x s.ordConnectedComponent x x s
    @[simp]
    theorem Set.nonempty_ordConnectedComponent {α : Type u_1} [LinearOrder α] {s : Set α} {x : α} :
    (s.ordConnectedComponent x).Nonempty x s
    @[simp]
    theorem Set.ordConnectedComponent_eq_empty {α : Type u_1} [LinearOrder α] {s : Set α} {x : α} :
    s.ordConnectedComponent x = xs
    @[simp]
    theorem Set.ordConnectedComponent_empty {α : Type u_1} [LinearOrder α] {x : α} :
    .ordConnectedComponent x =
    @[simp]
    theorem Set.ordConnectedComponent_univ {α : Type u_1} [LinearOrder α] {x : α} :
    Set.univ.ordConnectedComponent x = Set.univ
    theorem Set.ordConnectedComponent_inter {α : Type u_1} [LinearOrder α] (s : Set α) (t : Set α) (x : α) :
    (s t).ordConnectedComponent x = s.ordConnectedComponent x t.ordConnectedComponent x
    theorem Set.mem_ordConnectedComponent_comm {α : Type u_1} [LinearOrder α] {s : Set α} {x : α} {y : α} :
    y s.ordConnectedComponent x x s.ordConnectedComponent y
    theorem Set.mem_ordConnectedComponent_trans {α : Type u_1} [LinearOrder α] {s : Set α} {x : α} {y : α} {z : α} (hxy : y s.ordConnectedComponent x) (hyz : z s.ordConnectedComponent y) :
    z s.ordConnectedComponent x
    theorem Set.ordConnectedComponent_eq {α : Type u_1} [LinearOrder α] {s : Set α} {x : α} {y : α} (h : Set.uIcc x y s) :
    s.ordConnectedComponent x = s.ordConnectedComponent y
    instance Set.instOrdConnectedOrdConnectedComponent {α : Type u_1} [LinearOrder α] {s : Set α} {x : α} :
    (s.ordConnectedComponent x).OrdConnected
    Equations
    • =
    noncomputable def Set.ordConnectedProj {α : Type u_1} [LinearOrder α] (s : Set α) :
    sα

    Projection from s : Set α to α sending each order connected component of s to a single point of this component.

    Equations
    • s.ordConnectedProj x = .some
    Instances For
      theorem Set.ordConnectedProj_mem_ordConnectedComponent {α : Type u_1} [LinearOrder α] (s : Set α) (x : s) :
      s.ordConnectedProj x s.ordConnectedComponent x
      theorem Set.mem_ordConnectedComponent_ordConnectedProj {α : Type u_1} [LinearOrder α] (s : Set α) (x : s) :
      x s.ordConnectedComponent (s.ordConnectedProj x)
      @[simp]
      theorem Set.ordConnectedComponent_ordConnectedProj {α : Type u_1} [LinearOrder α] (s : Set α) (x : s) :
      s.ordConnectedComponent (s.ordConnectedProj x) = s.ordConnectedComponent x
      @[simp]
      theorem Set.ordConnectedProj_eq {α : Type u_1} [LinearOrder α] {s : Set α} {x : s} {y : s} :
      s.ordConnectedProj x = s.ordConnectedProj y Set.uIcc x y s
      def Set.ordConnectedSection {α : Type u_1} [LinearOrder α] (s : Set α) :
      Set α

      A set that intersects each order connected component of a set by a single point. Defined as the range of Set.ordConnectedProj s.

      Equations
      • s.ordConnectedSection = Set.range s.ordConnectedProj
      Instances For
        theorem Set.dual_ordConnectedSection {α : Type u_1} [LinearOrder α] (s : Set α) :
        (OrderDual.ofDual ⁻¹' s).ordConnectedSection = OrderDual.ofDual ⁻¹' s.ordConnectedSection
        theorem Set.ordConnectedSection_subset {α : Type u_1} [LinearOrder α] {s : Set α} :
        s.ordConnectedSection s
        theorem Set.eq_of_mem_ordConnectedSection_of_uIcc_subset {α : Type u_1} [LinearOrder α] {s : Set α} {x : α} {y : α} (hx : x s.ordConnectedSection) (hy : y s.ordConnectedSection) (h : Set.uIcc x y s) :
        x = y
        def Set.ordSeparatingSet {α : Type u_1} [LinearOrder α] (s : Set α) (t : Set α) :
        Set α

        Given two sets s t : Set α, the set Set.orderSeparatingSet s t is the set of points that belong both to some Set.ordConnectedComponent tᶜ x, x ∈ s, and to some Set.ordConnectedComponent sᶜ x, x ∈ t. In the case of two disjoint closed sets, this is the union of all open intervals $(a, b)$ such that their endpoints belong to different sets.

        Equations
        • s.ordSeparatingSet t = (⋃ xs, t.ordConnectedComponent x) xt, s.ordConnectedComponent x
        Instances For
          theorem Set.ordSeparatingSet_comm {α : Type u_1} [LinearOrder α] (s : Set α) (t : Set α) :
          s.ordSeparatingSet t = t.ordSeparatingSet s
          theorem Set.disjoint_left_ordSeparatingSet {α : Type u_1} [LinearOrder α] {s : Set α} {t : Set α} :
          Disjoint s (s.ordSeparatingSet t)
          theorem Set.disjoint_right_ordSeparatingSet {α : Type u_1} [LinearOrder α] {s : Set α} {t : Set α} :
          Disjoint t (s.ordSeparatingSet t)
          theorem Set.dual_ordSeparatingSet {α : Type u_1} [LinearOrder α] {s : Set α} {t : Set α} :
          (OrderDual.ofDual ⁻¹' s).ordSeparatingSet (OrderDual.ofDual ⁻¹' t) = OrderDual.ofDual ⁻¹' s.ordSeparatingSet t
          def Set.ordT5Nhd {α : Type u_1} [LinearOrder α] (s : Set α) (t : Set α) :
          Set α

          An auxiliary neighborhood that will be used in the proof of OrderTopology.CompletelyNormalSpace.

          Equations
          • s.ordT5Nhd t = xs, (t (s.ordSeparatingSet t).ordConnectedSection).ordConnectedComponent x
          Instances For
            theorem Set.disjoint_ordT5Nhd {α : Type u_1} [LinearOrder α] {s : Set α} {t : Set α} :
            Disjoint (s.ordT5Nhd t) (t.ordT5Nhd s)