Documentation

Mathlib.Order.Cover

The covering relation #

This file defines the covering relation in an order. b is said to cover a if a < b and there is no element in between. We say that b weakly covers a if a ≤ b and there is no element between a and b. In a partial order this is equivalent to a ⋖ b ∨ a = b, in a preorder this is equivalent to a ⋖ b ∨ (a ≤ b ∧ b ≤ a)

Notation #

def Wcovby {α : Type u_1} [Preorder α] (a : α) (b : α) :

Wcovby a b means that a = b or b covers a. This means that a ≤ b and there is no element in between.

Instances For

    Notation for Wcovby a b.

    Instances For
      theorem Wcovby.le {α : Type u_1} [Preorder α] {a : α} {b : α} (h : a ⩿ b) :
      a b
      theorem Wcovby.refl {α : Type u_1} [Preorder α] (a : α) :
      a ⩿ a
      theorem Wcovby.rfl {α : Type u_1} [Preorder α] {a : α} :
      a ⩿ a
      theorem Eq.wcovby {α : Type u_1} [Preorder α] {a : α} {b : α} (h : a = b) :
      a ⩿ b
      theorem wcovby_of_le_of_le {α : Type u_1} [Preorder α] {a : α} {b : α} (h1 : a b) (h2 : b a) :
      a ⩿ b
      theorem LE.le.wcovby_of_le {α : Type u_1} [Preorder α] {a : α} {b : α} (h1 : a b) (h2 : b a) :
      a ⩿ b

      Alias of wcovby_of_le_of_le.

      theorem AntisymmRel.wcovby {α : Type u_1} [Preorder α] {a : α} {b : α} (h : AntisymmRel (fun x x_1 => x x_1) a b) :
      a ⩿ b
      theorem Wcovby.wcovby_iff_le {α : Type u_1} [Preorder α] {a : α} {b : α} (hab : a ⩿ b) :
      b ⩿ a b a
      theorem wcovby_of_eq_or_eq {α : Type u_1} [Preorder α] {a : α} {b : α} (hab : a b) (h : ∀ (c : α), a cc bc = a c = b) :
      a ⩿ b
      theorem AntisymmRel.trans_wcovby {α : Type u_1} [Preorder α] {a : α} {b : α} {c : α} (hab : AntisymmRel (fun x x_1 => x x_1) a b) (hbc : b ⩿ c) :
      a ⩿ c
      theorem wcovby_congr_left {α : Type u_1} [Preorder α] {a : α} {b : α} {c : α} (hab : AntisymmRel (fun x x_1 => x x_1) a b) :
      a ⩿ c b ⩿ c
      theorem Wcovby.trans_antisymm_rel {α : Type u_1} [Preorder α] {a : α} {b : α} {c : α} (hab : a ⩿ b) (hbc : AntisymmRel (fun x x_1 => x x_1) b c) :
      a ⩿ c
      theorem wcovby_congr_right {α : Type u_1} [Preorder α] {a : α} {b : α} {c : α} (hab : AntisymmRel (fun x x_1 => x x_1) a b) :
      c ⩿ a c ⩿ b
      theorem not_wcovby_iff {α : Type u_1} [Preorder α] {a : α} {b : α} (h : a b) :
      ¬a ⩿ b c, a < c c < b

      If a ≤ b, then b does not cover a iff there's an element in between.

      instance Wcovby.isRefl {α : Type u_1} [Preorder α] :
      IsRefl α fun x x_1 => x ⩿ x_1
      theorem Wcovby.Ioo_eq {α : Type u_1} [Preorder α] {a : α} {b : α} (h : a ⩿ b) :
      theorem wcovby_iff_Ioo_eq {α : Type u_1} [Preorder α] {a : α} {b : α} :
      a ⩿ b a b Set.Ioo a b =
      theorem Wcovby.of_le_of_le {α : Type u_1} [Preorder α] {a : α} {b : α} {c : α} (hac : a ⩿ c) (hab : a b) (hbc : b c) :
      b ⩿ c
      theorem Wcovby.of_le_of_le' {α : Type u_1} [Preorder α] {a : α} {b : α} {c : α} (hac : a ⩿ c) (hab : a b) (hbc : b c) :
      a ⩿ b
      theorem Wcovby.of_image {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a : α} {b : α} (f : α ↪o β) (h : f a ⩿ f b) :
      a ⩿ b
      theorem Wcovby.image {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a : α} {b : α} (f : α ↪o β) (hab : a ⩿ b) (h : Set.OrdConnected (Set.range f)) :
      f a ⩿ f b
      theorem Set.OrdConnected.apply_wcovby_apply_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a : α} {b : α} (f : α ↪o β) (h : Set.OrdConnected (Set.range f)) :
      f a ⩿ f b a ⩿ b
      @[simp]
      theorem apply_wcovby_apply_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a : α} {b : α} {E : Type u_3} [OrderIsoClass E α β] (e : E) :
      e a ⩿ e b a ⩿ b
      @[simp]
      theorem toDual_wcovby_toDual_iff {α : Type u_1} [Preorder α] {a : α} {b : α} :
      OrderDual.toDual b ⩿ OrderDual.toDual a a ⩿ b
      @[simp]
      theorem ofDual_wcovby_ofDual_iff {α : Type u_1} [Preorder α] {a : αᵒᵈ} {b : αᵒᵈ} :
      OrderDual.ofDual a ⩿ OrderDual.ofDual b b ⩿ a
      theorem Wcovby.toDual {α : Type u_1} [Preorder α] {a : α} {b : α} :
      a ⩿ bOrderDual.toDual b ⩿ OrderDual.toDual a

      Alias of the reverse direction of toDual_wcovby_toDual_iff.

      theorem Wcovby.ofDual {α : Type u_1} [Preorder α] {a : αᵒᵈ} {b : αᵒᵈ} :
      b ⩿ aOrderDual.ofDual a ⩿ OrderDual.ofDual b

      Alias of the reverse direction of ofDual_wcovby_ofDual_iff.

      theorem Wcovby.eq_or_eq {α : Type u_1} [PartialOrder α] {a : α} {b : α} {c : α} (h : a ⩿ b) (h2 : a c) (h3 : c b) :
      c = a c = b
      theorem wcovby_iff_le_and_eq_or_eq {α : Type u_1} [PartialOrder α] {a : α} {b : α} :
      a ⩿ b a b ∀ (c : α), a cc bc = a c = b

      An iff version of Wcovby.eq_or_eq and wcovby_of_eq_or_eq.

      theorem Wcovby.le_and_le_iff {α : Type u_1} [PartialOrder α] {a : α} {b : α} {c : α} (h : a ⩿ b) :
      a c c b c = a c = b
      theorem Wcovby.Icc_eq {α : Type u_1} [PartialOrder α] {a : α} {b : α} (h : a ⩿ b) :
      Set.Icc a b = {a, b}
      theorem Wcovby.Ico_subset {α : Type u_1} [PartialOrder α] {a : α} {b : α} (h : a ⩿ b) :
      Set.Ico a b {a}
      theorem Wcovby.Ioc_subset {α : Type u_1} [PartialOrder α] {a : α} {b : α} (h : a ⩿ b) :
      Set.Ioc a b {b}
      theorem Wcovby.sup_eq {α : Type u_1} [SemilatticeSup α] {a : α} {b : α} {c : α} (hac : a ⩿ c) (hbc : b ⩿ c) (hab : a b) :
      a b = c
      theorem Wcovby.inf_eq {α : Type u_1} [SemilatticeInf α] {a : α} {b : α} {c : α} (hca : c ⩿ a) (hcb : c ⩿ b) (hab : a b) :
      a b = c
      def Covby {α : Type u_1} [LT α] (a : α) (b : α) :

      Covby a b means that b covers a: a < b and there is no element in between.

      Instances For

        Notation for Covby a b.

        Instances For
          theorem Covby.lt {α : Type u_1} [LT α] {a : α} {b : α} (h : a b) :
          a < b
          theorem not_covby_iff {α : Type u_1} [LT α] {a : α} {b : α} (h : a < b) :
          ¬a b c, a < c c < b

          If a < b, then b does not cover a iff there's an element in between.

          theorem exists_lt_lt_of_not_covby {α : Type u_1} [LT α] {a : α} {b : α} (h : a < b) :
          ¬a bc, a < c c < b

          Alias of the forward direction of not_covby_iff.


          If a < b, then b does not cover a iff there's an element in between.

          theorem LT.lt.exists_lt_lt {α : Type u_1} [LT α] {a : α} {b : α} (h : a < b) :
          ¬a bc, a < c c < b

          Alias of the forward direction of not_covby_iff.


          Alias of the forward direction of not_covby_iff.


          If a < b, then b does not cover a iff there's an element in between.

          theorem not_covby {α : Type u_1} [LT α] {a : α} {b : α} [DenselyOrdered α] :
          ¬a b

          In a dense order, nothing covers anything.

          theorem densely_ordered_iff_forall_not_covby {α : Type u_1} [LT α] :
          DenselyOrdered α ∀ (a b : α), ¬a b
          @[simp]
          theorem toDual_covby_toDual_iff {α : Type u_1} [LT α] {a : α} {b : α} :
          OrderDual.toDual b OrderDual.toDual a a b
          @[simp]
          theorem ofDual_covby_ofDual_iff {α : Type u_1} [LT α] {a : αᵒᵈ} {b : αᵒᵈ} :
          OrderDual.ofDual a OrderDual.ofDual b b a
          theorem Covby.toDual {α : Type u_1} [LT α] {a : α} {b : α} :
          a bOrderDual.toDual b OrderDual.toDual a

          Alias of the reverse direction of toDual_covby_toDual_iff.

          theorem Covby.ofDual {α : Type u_1} [LT α] {a : αᵒᵈ} {b : αᵒᵈ} :
          b aOrderDual.ofDual a OrderDual.ofDual b

          Alias of the reverse direction of ofDual_covby_ofDual_iff.

          theorem Covby.le {α : Type u_1} [Preorder α] {a : α} {b : α} (h : a b) :
          a b
          theorem Covby.ne {α : Type u_1} [Preorder α] {a : α} {b : α} (h : a b) :
          a b
          theorem Covby.ne' {α : Type u_1} [Preorder α] {a : α} {b : α} (h : a b) :
          b a
          theorem Covby.wcovby {α : Type u_1} [Preorder α] {a : α} {b : α} (h : a b) :
          a ⩿ b
          theorem Wcovby.covby_of_not_le {α : Type u_1} [Preorder α] {a : α} {b : α} (h : a ⩿ b) (h2 : ¬b a) :
          a b
          theorem Wcovby.covby_of_lt {α : Type u_1} [Preorder α] {a : α} {b : α} (h : a ⩿ b) (h2 : a < b) :
          a b
          theorem Covby.of_le_of_lt {α : Type u_1} [Preorder α] {a : α} {b : α} {c : α} (hac : a c) (hab : a b) (hbc : b < c) :
          b c
          theorem Covby.of_lt_of_le {α : Type u_1} [Preorder α] {a : α} {b : α} {c : α} (hac : a c) (hab : a < b) (hbc : b c) :
          a b
          theorem not_covby_of_lt_of_lt {α : Type u_1} [Preorder α] {a : α} {b : α} {c : α} (h₁ : a < b) (h₂ : b < c) :
          ¬a c
          theorem covby_iff_wcovby_and_lt {α : Type u_1} [Preorder α] {a : α} {b : α} :
          a b a ⩿ b a < b
          theorem covby_iff_wcovby_and_not_le {α : Type u_1} [Preorder α] {a : α} {b : α} :
          a b a ⩿ b ¬b a
          theorem wcovby_iff_covby_or_le_and_le {α : Type u_1} [Preorder α] {a : α} {b : α} :
          a ⩿ b a b a b b a
          theorem AntisymmRel.trans_covby {α : Type u_1} [Preorder α] {a : α} {b : α} {c : α} (hab : AntisymmRel (fun x x_1 => x x_1) a b) (hbc : b c) :
          a c
          theorem covby_congr_left {α : Type u_1} [Preorder α] {a : α} {b : α} {c : α} (hab : AntisymmRel (fun x x_1 => x x_1) a b) :
          a c b c
          theorem Covby.trans_antisymmRel {α : Type u_1} [Preorder α] {a : α} {b : α} {c : α} (hab : a b) (hbc : AntisymmRel (fun x x_1 => x x_1) b c) :
          a c
          theorem covby_congr_right {α : Type u_1} [Preorder α] {a : α} {b : α} {c : α} (hab : AntisymmRel (fun x x_1 => x x_1) a b) :
          c a c b
          instance instIsNonstrictStrictOrderWcovbyCovbyToLT {α : Type u_1} [Preorder α] :
          IsNonstrictStrictOrder α (fun x x_1 => x ⩿ x_1) fun x x_1 => x x_1
          instance Covby.isIrrefl {α : Type u_1} [Preorder α] :
          IsIrrefl α fun x x_1 => x x_1
          theorem Covby.Ioo_eq {α : Type u_1} [Preorder α] {a : α} {b : α} (h : a b) :
          theorem covby_iff_Ioo_eq {α : Type u_1} [Preorder α] {a : α} {b : α} :
          a b a < b Set.Ioo a b =
          theorem Covby.of_image {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a : α} {b : α} (f : α ↪o β) (h : f a f b) :
          a b
          theorem Covby.image {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a : α} {b : α} (f : α ↪o β) (hab : a b) (h : Set.OrdConnected (Set.range f)) :
          f a f b
          theorem Set.OrdConnected.apply_covby_apply_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a : α} {b : α} (f : α ↪o β) (h : Set.OrdConnected (Set.range f)) :
          f a f b a b
          @[simp]
          theorem apply_covby_apply_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a : α} {b : α} {E : Type u_3} [OrderIsoClass E α β] (e : E) :
          e a e b a b
          theorem covby_of_eq_or_eq {α : Type u_1} [Preorder α] {a : α} {b : α} (hab : a < b) (h : ∀ (c : α), a cc bc = a c = b) :
          a b
          theorem Wcovby.covby_of_ne {α : Type u_1} [PartialOrder α] {a : α} {b : α} (h : a ⩿ b) (h2 : a b) :
          a b
          theorem covby_iff_wcovby_and_ne {α : Type u_1} [PartialOrder α] {a : α} {b : α} :
          a b a ⩿ b a b
          theorem wcovby_iff_covby_or_eq {α : Type u_1} [PartialOrder α] {a : α} {b : α} :
          a ⩿ b a b a = b
          theorem wcovby_iff_eq_or_covby {α : Type u_1} [PartialOrder α] {a : α} {b : α} :
          a ⩿ b a = b a b
          theorem Wcovby.covby_or_eq {α : Type u_1} [PartialOrder α] {a : α} {b : α} :
          a ⩿ ba b a = b

          Alias of the forward direction of wcovby_iff_covby_or_eq.

          theorem Wcovby.eq_or_covby {α : Type u_1} [PartialOrder α] {a : α} {b : α} :
          a ⩿ ba = b a b

          Alias of the forward direction of wcovby_iff_eq_or_covby.

          theorem Covby.eq_or_eq {α : Type u_1} [PartialOrder α] {a : α} {b : α} {c : α} (h : a b) (h2 : a c) (h3 : c b) :
          c = a c = b
          theorem covby_iff_lt_and_eq_or_eq {α : Type u_1} [PartialOrder α] {a : α} {b : α} :
          a b a < b ∀ (c : α), a cc bc = a c = b

          An iff version of Covby.eq_or_eq and covby_of_eq_or_eq.

          theorem Covby.Ico_eq {α : Type u_1} [PartialOrder α] {a : α} {b : α} (h : a b) :
          Set.Ico a b = {a}
          theorem Covby.Ioc_eq {α : Type u_1} [PartialOrder α] {a : α} {b : α} (h : a b) :
          Set.Ioc a b = {b}
          theorem Covby.Icc_eq {α : Type u_1} [PartialOrder α] {a : α} {b : α} (h : a b) :
          Set.Icc a b = {a, b}
          theorem Covby.Ioi_eq {α : Type u_1} [LinearOrder α] {a : α} {b : α} (h : a b) :
          theorem Covby.Iio_eq {α : Type u_1} [LinearOrder α] {a : α} {b : α} (h : a b) :
          theorem Wcovby.le_of_lt {α : Type u_1} [LinearOrder α] {a : α} {b : α} {c : α} (hab : a ⩿ b) (hcb : c < b) :
          c a
          theorem Wcovby.ge_of_gt {α : Type u_1} [LinearOrder α] {a : α} {b : α} {c : α} (hab : a ⩿ b) (hac : a < c) :
          b c
          theorem Covby.le_of_lt {α : Type u_1} [LinearOrder α] {a : α} {b : α} {c : α} (hab : a b) :
          c < bc a
          theorem Covby.ge_of_gt {α : Type u_1} [LinearOrder α] {a : α} {b : α} {c : α} (hab : a b) :
          a < cb c
          theorem Covby.unique_left {α : Type u_1} [LinearOrder α] {a : α} {b : α} {c : α} (ha : a c) (hb : b c) :
          a = b
          theorem Covby.unique_right {α : Type u_1} [LinearOrder α] {a : α} {b : α} {c : α} (hb : a b) (hc : a c) :
          b = c
          theorem Covby.eq_of_between {α : Type u_1} [LinearOrder α] {a : α} {b : α} {c : α} {x : α} (hab : a b) (hbc : b c) (hax : a < x) (hxc : x < c) :
          x = b

          If a, b, c are consecutive and a < x < c then x = b.

          theorem LT.lt.exists_disjoint_Iio_Ioi {α : Type u_1} [LinearOrder α] {a : α} {b : α} (h : a < b) :
          a', a' > a b', b' < b ∀ (x : α), x < a'∀ (y : α), y > b'x < y

          If a < b then there exist a' > a and b' < b such that Set.Iio a' is strictly to the left of Set.Ioi b'.

          theorem Set.wcovby_insert {α : Type u_1} (x : α) (s : Set α) :
          s ⩿ insert x s
          theorem Set.covby_insert {α : Type u_1} {x : α} {s : Set α} (hx : ¬x s) :
          s insert x s
          theorem wcovby_eq_reflGen_covby {α : Type u_1} [PartialOrder α] :
          (fun x x_1 => x ⩿ x_1) = Relation.ReflGen fun x x_1 => x x_1
          theorem transGen_wcovby_eq_reflTransGen_covby {α : Type u_1} [PartialOrder α] :
          (Relation.TransGen fun x x_1 => x ⩿ x_1) = Relation.ReflTransGen fun x x_1 => x x_1
          @[simp]
          theorem Prod.swap_wcovby_swap {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {x : α × β} {y : α × β} :
          @[simp]
          theorem Prod.swap_covby_swap {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {x : α × β} {y : α × β} :
          theorem Prod.fst_eq_or_snd_eq_of_wcovby {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {x : α × β} {y : α × β} :
          x ⩿ yx.fst = y.fst x.snd = y.snd
          theorem Wcovby.fst {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {x : α × β} {y : α × β} (h : x ⩿ y) :
          x.fst ⩿ y.fst
          theorem Wcovby.snd {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {x : α × β} {y : α × β} (h : x ⩿ y) :
          x.snd ⩿ y.snd
          theorem Prod.mk_wcovby_mk_iff_left {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {a₁ : α} {a₂ : α} {b : β} :
          (a₁, b) ⩿ (a₂, b) a₁ ⩿ a₂
          theorem Prod.mk_wcovby_mk_iff_right {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {a : α} {b₁ : β} {b₂ : β} :
          (a, b₁) ⩿ (a, b₂) b₁ ⩿ b₂
          theorem Prod.mk_covby_mk_iff_left {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {a₁ : α} {a₂ : α} {b : β} :
          (a₁, b) (a₂, b) a₁ a₂
          theorem Prod.mk_covby_mk_iff_right {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {a : α} {b₁ : β} {b₂ : β} :
          (a, b₁) (a, b₂) b₁ b₂
          theorem Prod.mk_wcovby_mk_iff {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} :
          (a₁, b₁) ⩿ (a₂, b₂) a₁ ⩿ a₂ b₁ = b₂ b₁ ⩿ b₂ a₁ = a₂
          theorem Prod.mk_covby_mk_iff {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {a₁ : α} {a₂ : α} {b₁ : β} {b₂ : β} :
          (a₁, b₁) (a₂, b₂) a₁ a₂ b₁ = b₂ b₁ b₂ a₁ = a₂
          theorem Prod.wcovby_iff {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {x : α × β} {y : α × β} :
          x ⩿ y x.fst ⩿ y.fst x.snd = y.snd x.snd ⩿ y.snd x.fst = y.fst
          theorem Prod.covby_iff {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {x : α × β} {y : α × β} :
          x y x.fst y.fst x.snd = y.snd x.snd y.snd x.fst = y.fst