# 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 #

• a ⋖ b means that b covers a.
• a ⩿ b means that b weakly covers a.
def WCovBy {α : Type u_1} [] (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.

Equations
Instances For

Notation for WCovBy a b.

Equations
Instances For
theorem WCovBy.le {α : Type u_1} [] {a : α} {b : α} (h : a ⩿ b) :
a b
theorem WCovBy.refl {α : Type u_1} [] (a : α) :
a ⩿ a
@[simp]
theorem WCovBy.rfl {α : Type u_1} [] {a : α} :
a ⩿ a
theorem Eq.wcovBy {α : Type u_1} [] {a : α} {b : α} (h : a = b) :
a ⩿ b
theorem wcovBy_of_le_of_le {α : Type u_1} [] {a : α} {b : α} (h1 : a b) (h2 : b a) :
a ⩿ b
theorem LE.le.wcovBy_of_le {α : Type u_1} [] {a : α} {b : α} (h1 : a b) (h2 : b a) :
a ⩿ b

Alias of wcovBy_of_le_of_le.

theorem AntisymmRel.wcovBy {α : Type u_1} [] {a : α} {b : α} (h : AntisymmRel (fun (x1 x2 : α) => x1 x2) a b) :
a ⩿ b
theorem WCovBy.wcovBy_iff_le {α : Type u_1} [] {a : α} {b : α} (hab : a ⩿ b) :
b ⩿ a b a
theorem wcovBy_of_eq_or_eq {α : Type u_1} [] {a : α} {b : α} (hab : a b) (h : ∀ (c : α), a cc bc = a c = b) :
a ⩿ b
theorem AntisymmRel.trans_wcovBy {α : Type u_1} [] {a : α} {b : α} {c : α} (hab : AntisymmRel (fun (x1 x2 : α) => x1 x2) a b) (hbc : b ⩿ c) :
a ⩿ c
theorem wcovBy_congr_left {α : Type u_1} [] {a : α} {b : α} {c : α} (hab : AntisymmRel (fun (x1 x2 : α) => x1 x2) a b) :
a ⩿ c b ⩿ c
theorem WCovBy.trans_antisymm_rel {α : Type u_1} [] {a : α} {b : α} {c : α} (hab : a ⩿ b) (hbc : AntisymmRel (fun (x1 x2 : α) => x1 x2) b c) :
a ⩿ c
theorem wcovBy_congr_right {α : Type u_1} [] {a : α} {b : α} {c : α} (hab : AntisymmRel (fun (x1 x2 : α) => x1 x2) a b) :
c ⩿ a c ⩿ b
theorem not_wcovBy_iff {α : Type u_1} [] {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} [] :
IsRefl α fun (x1 x2 : α) => x1 ⩿ x2
Equations
• =
theorem WCovBy.Ioo_eq {α : Type u_1} [] {a : α} {b : α} (h : a ⩿ b) :
theorem wcovBy_iff_Ioo_eq {α : Type u_1} [] {a : α} {b : α} :
a ⩿ b a b Set.Ioo a b =
theorem WCovBy.of_le_of_le {α : Type u_1} [] {a : α} {b : α} {c : α} (hac : a ⩿ c) (hab : a b) (hbc : b c) :
b ⩿ c
theorem WCovBy.of_le_of_le' {α : Type u_1} [] {a : α} {b : α} {c : α} (hac : a ⩿ c) (hab : a b) (hbc : b c) :
a ⩿ b
theorem WCovBy.of_image {α : Type u_1} {β : Type u_2} [] [] {a : α} {b : α} (f : α ↪o β) (h : f a ⩿ f b) :
a ⩿ b
theorem WCovBy.image {α : Type u_1} {β : Type u_2} [] [] {a : α} {b : α} (f : α ↪o β) (hab : a ⩿ b) (h : (Set.range f).OrdConnected) :
f a ⩿ f b
theorem Set.OrdConnected.apply_wcovBy_apply_iff {α : Type u_1} {β : Type u_2} [] [] {a : α} {b : α} (f : α ↪o β) (h : (Set.range f).OrdConnected) :
f a ⩿ f b a ⩿ b
@[simp]
theorem apply_wcovBy_apply_iff {α : Type u_1} {β : Type u_2} [] [] {a : α} {b : α} {E : Type u_3} [EquivLike E α β] [] (e : E) :
e a ⩿ e b a ⩿ b
@[simp]
theorem toDual_wcovBy_toDual_iff {α : Type u_1} [] {a : α} {b : α} :
OrderDual.toDual b ⩿ OrderDual.toDual a a ⩿ b
@[simp]
theorem ofDual_wcovBy_ofDual_iff {α : Type u_1} [] {a : αᵒᵈ} {b : αᵒᵈ} :
OrderDual.ofDual a ⩿ OrderDual.ofDual b b ⩿ a
theorem WCovBy.toDual {α : Type u_1} [] {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} [] {a : αᵒᵈ} {b : αᵒᵈ} :
b ⩿ aOrderDual.ofDual a ⩿ OrderDual.ofDual b

Alias of the reverse direction of ofDual_wcovBy_ofDual_iff.

theorem OrderEmbedding.wcovBy_of_apply {α : Type u_3} {β : Type u_4} [] [] (f : α ↪o β) {x : α} {y : α} (h : f x ⩿ f y) :
x ⩿ y
theorem OrderIso.map_wcovBy {α : Type u_3} {β : Type u_4} [] [] (f : α ≃o β) {x : α} {y : α} :
f x ⩿ f y x ⩿ y
theorem WCovBy.eq_or_eq {α : Type u_1} [] {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} [] {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} [] {a : α} {b : α} {c : α} (h : a ⩿ b) :
a c c b c = a c = b
theorem WCovBy.Icc_eq {α : Type u_1} [] {a : α} {b : α} (h : a ⩿ b) :
Set.Icc a b = {a, b}
theorem WCovBy.Ico_subset {α : Type u_1} [] {a : α} {b : α} (h : a ⩿ b) :
Set.Ico a b {a}
theorem WCovBy.Ioc_subset {α : Type u_1} [] {a : α} {b : α} (h : a ⩿ b) :
Set.Ioc a b {b}
theorem WCovBy.sup_eq {α : Type u_1} [] {a : α} {b : α} {c : α} (hac : a ⩿ c) (hbc : b ⩿ c) (hab : a b) :
a b = c
theorem WCovBy.inf_eq {α : Type u_1} [] {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.

Equations
Instances For

Notation for CovBy a b.

Equations
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 b∃ (c : α), 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 b∃ (c : α), 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 : α} [] :
¬a b

In a dense order, nothing covers anything.

theorem denselyOrdered_iff_forall_not_covBy {α : Type u_1} [LT α] :
∀ (a b : α), ¬a b
@[deprecated denselyOrdered_iff_forall_not_covBy]
theorem densely_ordered_iff_forall_not_covBy {α : Type u_1} [LT α] :
∀ (a b : α), ¬a b

Alias of denselyOrdered_iff_forall_not_covBy.

@[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} [] {a : α} {b : α} (h : a b) :
a b
theorem CovBy.ne {α : Type u_1} [] {a : α} {b : α} (h : a b) :
a b
theorem CovBy.ne' {α : Type u_1} [] {a : α} {b : α} (h : a b) :
b a
theorem CovBy.wcovBy {α : Type u_1} [] {a : α} {b : α} (h : a b) :
a ⩿ b
theorem WCovBy.covBy_of_not_le {α : Type u_1} [] {a : α} {b : α} (h : a ⩿ b) (h2 : ¬b a) :
a b
theorem WCovBy.covBy_of_lt {α : Type u_1} [] {a : α} {b : α} (h : a ⩿ b) (h2 : a < b) :
a b
theorem CovBy.of_le_of_lt {α : Type u_1} [] {a : α} {b : α} {c : α} (hac : a c) (hab : a b) (hbc : b < c) :
b c
theorem CovBy.of_lt_of_le {α : Type u_1} [] {a : α} {b : α} {c : α} (hac : a c) (hab : a < b) (hbc : b c) :
a b
theorem not_covBy_of_lt_of_lt {α : Type u_1} [] {a : α} {b : α} {c : α} (h₁ : a < b) (h₂ : b < c) :
¬a c
theorem covBy_iff_wcovBy_and_lt {α : Type u_1} [] {a : α} {b : α} :
a b a ⩿ b a < b
theorem covBy_iff_wcovBy_and_not_le {α : Type u_1} [] {a : α} {b : α} :
a b a ⩿ b ¬b a
theorem wcovBy_iff_covBy_or_le_and_le {α : Type u_1} [] {a : α} {b : α} :
a ⩿ b a b a b b a
theorem WCovBy.covBy_or_le_and_le {α : Type u_1} [] {a : α} {b : α} :
a ⩿ ba b a b b a

Alias of the forward direction of wcovBy_iff_covBy_or_le_and_le.

theorem AntisymmRel.trans_covBy {α : Type u_1} [] {a : α} {b : α} {c : α} (hab : AntisymmRel (fun (x1 x2 : α) => x1 x2) a b) (hbc : b c) :
a c
theorem covBy_congr_left {α : Type u_1} [] {a : α} {b : α} {c : α} (hab : AntisymmRel (fun (x1 x2 : α) => x1 x2) a b) :
a c b c
theorem CovBy.trans_antisymmRel {α : Type u_1} [] {a : α} {b : α} {c : α} (hab : a b) (hbc : AntisymmRel (fun (x1 x2 : α) => x1 x2) b c) :
a c
theorem covBy_congr_right {α : Type u_1} [] {a : α} {b : α} {c : α} (hab : AntisymmRel (fun (x1 x2 : α) => x1 x2) a b) :
c a c b
instance instIsNonstrictStrictOrderWCovByCovBy {α : Type u_1} [] :
IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 ⩿ x2) fun (x1 x2 : α) => x1 x2
Equations
• =
instance CovBy.isIrrefl {α : Type u_1} [] :
IsIrrefl α fun (x1 x2 : α) => x1 x2
Equations
• =
theorem CovBy.Ioo_eq {α : Type u_1} [] {a : α} {b : α} (h : a b) :
theorem covBy_iff_Ioo_eq {α : Type u_1} [] {a : α} {b : α} :
a b a < b Set.Ioo a b =
theorem CovBy.of_image {α : Type u_1} {β : Type u_2} [] [] {a : α} {b : α} (f : α ↪o β) (h : f a f b) :
a b
theorem CovBy.image {α : Type u_1} {β : Type u_2} [] [] {a : α} {b : α} (f : α ↪o β) (hab : a b) (h : (Set.range f).OrdConnected) :
f a f b
theorem Set.OrdConnected.apply_covBy_apply_iff {α : Type u_1} {β : Type u_2} [] [] {a : α} {b : α} (f : α ↪o β) (h : (Set.range f).OrdConnected) :
f a f b a b
@[simp]
theorem apply_covBy_apply_iff {α : Type u_1} {β : Type u_2} [] [] {a : α} {b : α} {E : Type u_3} [EquivLike E α β] [] (e : E) :
e a e b a b
theorem covBy_of_eq_or_eq {α : Type u_1} [] {a : α} {b : α} (hab : a < b) (h : ∀ (c : α), a cc bc = a c = b) :
a b
theorem OrderEmbedding.covBy_of_apply {α : Type u_3} {β : Type u_4} [] [] (f : α ↪o β) {x : α} {y : α} (h : f x f y) :
x y
theorem OrderIso.map_covBy {α : Type u_3} {β : Type u_4} [] [] (f : α ≃o β) {x : α} {y : α} :
f x f y x y
theorem WCovBy.covBy_of_ne {α : Type u_1} [] {a : α} {b : α} (h : a ⩿ b) (h2 : a b) :
a b
theorem covBy_iff_wcovBy_and_ne {α : Type u_1} [] {a : α} {b : α} :
a b a ⩿ b a b
theorem wcovBy_iff_covBy_or_eq {α : Type u_1} [] {a : α} {b : α} :
a ⩿ b a b a = b
theorem wcovBy_iff_eq_or_covBy {α : Type u_1} [] {a : α} {b : α} :
a ⩿ b a = b a b
theorem WCovBy.covBy_or_eq {α : Type u_1} [] {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} [] {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} [] {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} [] {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} [] {a : α} {b : α} (h : a b) :
Set.Ico a b = {a}
theorem CovBy.Ioc_eq {α : Type u_1} [] {a : α} {b : α} (h : a b) :
Set.Ioc a b = {b}
theorem CovBy.Icc_eq {α : Type u_1} [] {a : α} {b : α} (h : a b) :
Set.Icc a b = {a, b}
theorem CovBy.Ioi_eq {α : Type u_1} [] {a : α} {b : α} (h : a b) :
=
theorem CovBy.Iio_eq {α : Type u_1} [] {a : α} {b : α} (h : a b) :
=
theorem WCovBy.le_of_lt {α : Type u_1} [] {a : α} {b : α} {c : α} (hab : a ⩿ b) (hcb : c < b) :
c a
theorem WCovBy.ge_of_gt {α : Type u_1} [] {a : α} {b : α} {c : α} (hab : a ⩿ b) (hac : a < c) :
b c
theorem CovBy.le_of_lt {α : Type u_1} [] {a : α} {b : α} {c : α} (hab : a b) :
c < bc a
theorem CovBy.ge_of_gt {α : Type u_1} [] {a : α} {b : α} {c : α} (hab : a b) :
a < cb c
theorem CovBy.unique_left {α : Type u_1} [] {a : α} {b : α} {c : α} (ha : a c) (hb : b c) :
a = b
theorem CovBy.unique_right {α : Type u_1} [] {a : α} {b : α} {c : α} (hb : a b) (hc : a c) :
b = c
theorem CovBy.eq_of_between {α : Type u_1} [] {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} [] {a : α} {b : α} (h : a < b) :
a' > a, b' < b, x < a', 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'.

@[simp]
theorem Set.wcovBy_insert {α : Type u_1} (x : α) (s : Set α) :
s ⩿ insert x s
@[simp]
theorem Set.sdiff_singleton_wcovBy {α : Type u_1} (s : Set α) (a : α) :
s \ {a} ⩿ s
@[simp]
theorem Set.covBy_insert {α : Type u_1} {s : Set α} {a : α} (ha : as) :
s insert a s
@[simp]
theorem Set.sdiff_singleton_covBy {α : Type u_1} {s : Set α} {a : α} (ha : a s) :
s \ {a} s
theorem CovBy.exists_set_insert {α : Type u_1} {s : Set α} {t : Set α} (h : s t) :
as, insert a s = t
theorem CovBy.exists_set_sdiff_singleton {α : Type u_1} {s : Set α} {t : Set α} (h : s t) :
at, t \ {a} = s
theorem Set.covBy_iff_exists_insert {α : Type u_1} {s : Set α} {t : Set α} :
s t as, insert a s = t
theorem Set.covBy_iff_exists_sdiff_singleton {α : Type u_1} {s : Set α} {t : Set α} :
s t at, t \ {a} = s
theorem wcovBy_eq_reflGen_covBy {α : Type u_1} [] :
(fun (x1 x2 : α) => x1 ⩿ x2) = Relation.ReflGen fun (x1 x2 : α) => x1 x2
theorem transGen_wcovBy_eq_reflTransGen_covBy {α : Type u_1} [] :
(Relation.TransGen fun (x1 x2 : α) => x1 ⩿ x2) = Relation.ReflTransGen fun (x1 x2 : α) => x1 x2
theorem reflTransGen_wcovBy_eq_reflTransGen_covBy {α : Type u_1} [] :
(Relation.ReflTransGen fun (x1 x2 : α) => x1 ⩿ x2) = Relation.ReflTransGen fun (x1 x2 : α) => x1 x2
@[simp]
theorem Prod.swap_wcovBy_swap {α : Type u_1} {β : Type u_2} [] [] {x : α × β} {y : α × β} :
x.swap ⩿ y.swap x ⩿ y
@[simp]
theorem Prod.swap_covBy_swap {α : Type u_1} {β : Type u_2} [] [] {x : α × β} {y : α × β} :
x.swap y.swap x y
theorem Prod.fst_eq_or_snd_eq_of_wcovBy {α : Type u_1} {β : Type u_2} [] [] {x : α × β} {y : α × β} :
x ⩿ yx.1 = y.1 x.2 = y.2
theorem WCovBy.fst {α : Type u_1} {β : Type u_2} [] [] {x : α × β} {y : α × β} (h : x ⩿ y) :
x.1 ⩿ y.1
theorem WCovBy.snd {α : Type u_1} {β : Type u_2} [] [] {x : α × β} {y : α × β} (h : x ⩿ y) :
x.2 ⩿ y.2
theorem Prod.mk_wcovBy_mk_iff_left {α : Type u_1} {β : Type u_2} [] [] {a₁ : α} {a₂ : α} {b : β} :
(a₁, b) ⩿ (a₂, b) a₁ ⩿ a₂
theorem Prod.mk_wcovBy_mk_iff_right {α : Type u_1} {β : Type u_2} [] [] {a : α} {b₁ : β} {b₂ : β} :
(a, b₁) ⩿ (a, b₂) b₁ ⩿ b₂
theorem Prod.mk_covBy_mk_iff_left {α : Type u_1} {β : Type u_2} [] [] {a₁ : α} {a₂ : α} {b : β} :
(a₁, b) (a₂, b) a₁ a₂
theorem Prod.mk_covBy_mk_iff_right {α : Type u_1} {β : Type u_2} [] [] {a : α} {b₁ : β} {b₂ : β} :
(a, b₁) (a, b₂) b₁ b₂
theorem Prod.mk_wcovBy_mk_iff {α : Type u_1} {β : Type u_2} [] [] {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} [] [] {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} [] [] {x : α × β} {y : α × β} :
x ⩿ y x.1 ⩿ y.1 x.2 = y.2 x.2 ⩿ y.2 x.1 = y.1
theorem Prod.covBy_iff {α : Type u_1} {β : Type u_2} [] [] {x : α × β} {y : α × β} :
x y x.1 y.1 x.2 = y.2 x.2 y.2 x.1 = y.1
@[simp]
theorem WithTop.coe_wcovBy_coe {α : Type u_1} [] {a : α} {b : α} :
a ⩿ b a ⩿ b
@[simp]
theorem WithTop.coe_covBy_coe {α : Type u_1} [] {a : α} {b : α} :
a b a b
@[simp]
theorem WithTop.coe_covBy_top {α : Type u_1} [] {a : α} :
a
@[simp]
theorem WithTop.coe_wcovBy_top {α : Type u_1} [] {a : α} :
a ⩿
@[simp]
theorem WithBot.coe_wcovBy_coe {α : Type u_1} [] {a : α} {b : α} :
a ⩿ b a ⩿ b
@[simp]
theorem WithBot.coe_covBy_coe {α : Type u_1} [] {a : α} {b : α} :
a b a b
@[simp]
theorem WithBot.bot_covBy_coe {α : Type u_1} [] {a : α} :
a
@[simp]
theorem WithBot.bot_wcovBy_coe {α : Type u_1} [] {a : α} :
⩿ a