# The covering relation #

This file proves properties of the covering relation in an order. We say that `b` covers `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`.

source
theorem WCovBy.le {α : Type u_1} [Preorder α] {a b : α} (h : a ⩿ b) :
a ≤ b
source
theorem WCovBy.refl {α : Type u_1} [Preorder α] (a : α) :
a ⩿ a
source
@[simp]
theorem WCovBy.rfl {α : Type u_1} [Preorder α] {a : α} :
a ⩿ a
source
theorem Eq.wcovBy {α : Type u_1} [Preorder α] {a b : α} (h : a = b) :
a ⩿ b
source
theorem wcovBy_of_le_of_le {α : Type u_1} [Preorder α] {a b : α} (h1 : a ≤ b) (h2 : b ≤ a) :
a ⩿ b
source
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`.

source
theorem AntisymmRel.wcovBy {α : Type u_1} [Preorder α] {a b : α} (h : AntisymmRel (fun (x1 x2 : α) => x1 ≤ x2) a b) :
a ⩿ b
source
theorem WCovBy.wcovBy_iff_le {α : Type u_1} [Preorder α] {a b : α} (hab : a ⩿ b) :
b ⩿ a ↔ b ≤ a
source
theorem wcovBy_of_eq_or_eq {α : Type u_1} [Preorder α] {a b : α} (hab : a ≤ b) (h : ∀ (c : α), a ≤ c → c ≤ b → c = a ∨ c = b) :
a ⩿ b
source
theorem AntisymmRel.trans_wcovBy {α : Type u_1} [Preorder α] {a b c : α} (hab : AntisymmRel (fun (x1 x2 : α) => x1 ≤ x2) a b) (hbc : b ⩿ c) :
a ⩿ c
source
theorem wcovBy_congr_left {α : Type u_1} [Preorder α] {a b c : α} (hab : AntisymmRel (fun (x1 x2 : α) => x1 ≤ x2) a b) :
a ⩿ c ↔ b ⩿ c
source
theorem WCovBy.trans_antisymm_rel {α : Type u_1} [Preorder α] {a b c : α} (hab : a ⩿ b) (hbc : AntisymmRel (fun (x1 x2 : α) => x1 ≤ x2) b c) :
a ⩿ c
source
theorem wcovBy_congr_right {α : Type u_1} [Preorder α] {a b c : α} (hab : AntisymmRel (fun (x1 x2 : α) => x1 ≤ x2) a b) :
c ⩿ a ↔ c ⩿ b
source
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.

source
instance WCovBy.isRefl {α : Type u_1} [Preorder α] :
IsRefl α fun (x1 x2 : α) => x1 ⩿ x2
source
theorem WCovBy.Ioo_eq {α : Type u_1} [Preorder α] {a b : α} (h : a ⩿ b) :
Set.Ioo a b = ∅
source
theorem wcovBy_iff_Ioo_eq {α : Type u_1} [Preorder α] {a b : α} :
a ⩿ b ↔ a ≤ b ∧ Set.Ioo a b = ∅
source
theorem WCovBy.of_le_of_le {α : Type u_1} [Preorder α] {a b c : α} (hac : a ⩿ c) (hab : a ≤ b) (hbc : b ≤ c) :
b ⩿ c
source
theorem WCovBy.of_le_of_le' {α : Type u_1} [Preorder α] {a b c : α} (hac : a ⩿ c) (hab : a ≤ b) (hbc : b ≤ c) :
a ⩿ b
source
theorem WCovBy.of_image {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a b : α} (f : α ↪o β) (h : f a ⩿ f b) :
a ⩿ b
source
theorem WCovBy.image {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a b : α} (f : α ↪o β) (hab : a ⩿ b) (h : (Set.range ⇑f).OrdConnected) :
f a ⩿ f b
source
theorem Set.OrdConnected.apply_wcovBy_apply_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a b : α} (f : α ↪o β) (h : (range ⇑f).OrdConnected) :
f a ⩿ f b ↔ a ⩿ b
source
@[simp]
theorem apply_wcovBy_apply_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a b : α} {E : Type u_3} [EquivLike E α β] [OrderIsoClass E α β] (e : E) :
e a ⩿ e b ↔ a ⩿ b
source
@[simp]
theorem toDual_wcovBy_toDual_iff {α : Type u_1} [Preorder α] {a b : α} :
OrderDual.toDual b ⩿ OrderDual.toDual a ↔ a ⩿ b
source
@[simp]
theorem ofDual_wcovBy_ofDual_iff {α : Type u_1} [Preorder α] {a b : α ᵒᵈ} :
OrderDual.ofDual a ⩿ OrderDual.ofDual b ↔ b ⩿ a
source
theorem WCovBy.toDual {α : Type u_1} [Preorder α] {a b : α} :
a ⩿ b → OrderDual.toDual b ⩿ OrderDual.toDual a

Alias of the reverse direction of `toDual_wcovBy_toDual_iff`.

source
theorem WCovBy.ofDual {α : Type u_1} [Preorder α] {a b : α ᵒᵈ} :
b ⩿ a → OrderDual.ofDual a ⩿ OrderDual.ofDual b

Alias of the reverse direction of `ofDual_wcovBy_ofDual_iff`.

source
@[deprecated WCovBy.of_image (since := "2025-11-07")]
theorem OrderEmbedding.wcovBy_of_apply {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a b : α} (f : α ↪o β) (h : f a ⩿ f b) :
a ⩿ b

Alias of `WCovBy.of_image`.

source
@[deprecated apply_wcovBy_apply_iff (since := "2025-11-07")]
theorem OrderIso.map_wcovBy {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a b : α} {E : Type u_3} [EquivLike E α β] [OrderIsoClass E α β] (e : E) :
e a ⩿ e b ↔ a ⩿ b

Alias of `apply_wcovBy_apply_iff`.

source
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
source
theorem wcovBy_iff_le_and_eq_or_eq {α : Type u_1} [PartialOrder α] {a b : α} :
a ⩿ b ↔ a ≤ b ∧ ∀ (c : α), a ≤ c → c ≤ b → c = a ∨ c = b

An `iff` version of `WCovBy.eq_or_eq` and `wcovBy_of_eq_or_eq`.

source
theorem WCovBy.le_and_le_iff {α : Type u_1} [PartialOrder α] {a b c : α} (h : a ⩿ b) :
a ≤ c ∧ c ≤ b ↔ c = a ∨ c = b
source
theorem WCovBy.Icc_eq {α : Type u_1} [PartialOrder α] {a b : α} (h : a ⩿ b) :
Set.Icc a b = {a, b}
source
theorem WCovBy.Ico_subset {α : Type u_1} [PartialOrder α] {a b : α} (h : a ⩿ b) :
Set.Ico a b ⊆ {a}
source
theorem WCovBy.Ioc_subset {α : Type u_1} [PartialOrder α] {a b : α} (h : a ⩿ b) :
Set.Ioc a b ⊆ {b}
source
theorem WCovBy.sup_eq {α : Type u_1} [SemilatticeSup α] {a b c : α} (hac : a ⩿ c) (hbc : b ⩿ c) (hab : a ≠ b) :
a ⊔ b = c
source
theorem WCovBy.inf_eq {α : Type u_1} [SemilatticeInf α] {a b c : α} (hca : c ⩿ a) (hcb : c ⩿ b) (hab : a ≠ b) :
a ⊓ b = c
source
theorem CovBy.lt {α : Type u_1} [LT α] {a b : α} (h : a ⋖ b) :
a < b
source
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.

source
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.

source
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.

source
theorem not_covBy {α : Type u_1} [LT α] {a b : α} [DenselyOrdered α] :
¬a ⋖ b

In a dense order, nothing covers anything.

source
theorem denselyOrdered_iff_forall_not_covBy {α : Type u_1} [LT α] :
DenselyOrdered α ↔ ∀ (a b : α), ¬a ⋖ b
source
@[simp]
theorem toDual_covBy_toDual_iff {α : Type u_1} [LT α] {a b : α} :
OrderDual.toDual b ⋖ OrderDual.toDual a ↔ a ⋖ b
source
@[simp]
theorem ofDual_covBy_ofDual_iff {α : Type u_1} [LT α] {a b : α ᵒᵈ} :
OrderDual.ofDual a ⋖ OrderDual.ofDual b ↔ b ⋖ a
source
theorem CovBy.toDual {α : Type u_1} [LT α] {a b : α} :
a ⋖ b → OrderDual.toDual b ⋖ OrderDual.toDual a

Alias of the reverse direction of `toDual_covBy_toDual_iff`.

source
theorem CovBy.ofDual {α : Type u_1} [LT α] {a b : α ᵒᵈ} :
b ⋖ a → OrderDual.ofDual a ⋖ OrderDual.ofDual b

Alias of the reverse direction of `ofDual_covBy_ofDual_iff`.

source
theorem CovBy.le {α : Type u_1} [Preorder α] {a b : α} (h : a ⋖ b) :
a ≤ b
source
theorem CovBy.ne {α : Type u_1} [Preorder α] {a b : α} (h : a ⋖ b) :
a ≠ b
source
theorem CovBy.ne' {α : Type u_1} [Preorder α] {a b : α} (h : a ⋖ b) :
b ≠ a
source
theorem CovBy.wcovBy {α : Type u_1} [Preorder α] {a b : α} (h : a ⋖ b) :
a ⩿ b
source
theorem WCovBy.covBy_of_not_le {α : Type u_1} [Preorder α] {a b : α} (h : a ⩿ b) (h2 : ¬b ≤ a) :
a ⋖ b
source
theorem WCovBy.covBy_of_lt {α : Type u_1} [Preorder α] {a b : α} (h : a ⩿ b) (h2 : a < b) :
a ⋖ b
source
theorem CovBy.of_le_of_lt {α : Type u_1} [Preorder α] {a b c : α} (hac : a ⋖ c) (hab : a ≤ b) (hbc : b < c) :
b ⋖ c
source
theorem CovBy.of_lt_of_le {α : Type u_1} [Preorder α] {a b c : α} (hac : a ⋖ c) (hab : a < b) (hbc : b ≤ c) :
a ⋖ b
source
theorem not_covBy_of_lt_of_lt {α : Type u_1} [Preorder α] {a b c : α} (h₁ : a < b) (h₂ : b < c) :
¬a ⋖ c
source
theorem covBy_iff_wcovBy_and_lt {α : Type u_1} [Preorder α] {a b : α} :
a ⋖ b ↔ a ⩿ b ∧ a < b
source
theorem covBy_iff_wcovBy_and_not_le {α : Type u_1} [Preorder α] {a b : α} :
a ⋖ b ↔ a ⩿ b ∧ ¬b ≤ a
source
theorem wcovBy_iff_covBy_or_le_and_le {α : Type u_1} [Preorder α] {a b : α} :
a ⩿ b ↔ a ⋖ b ∨ a ≤ b ∧ b ≤ a
source
theorem WCovBy.covBy_or_le_and_le {α : Type u_1} [Preorder α] {a b : α} :
a ⩿ b → a ⋖ b ∨ a ≤ b ∧ b ≤ a

Alias of the forward direction of `wcovBy_iff_covBy_or_le_and_le`.

source
theorem AntisymmRel.trans_covBy {α : Type u_1} [Preorder α] {a b c : α} (hab : AntisymmRel (fun (x1 x2 : α) => x1 ≤ x2) a b) (hbc : b ⋖ c) :
a ⋖ c
source
theorem covBy_congr_left {α : Type u_1} [Preorder α] {a b c : α} (hab : AntisymmRel (fun (x1 x2 : α) => x1 ≤ x2) a b) :
a ⋖ c ↔ b ⋖ c
source
theorem CovBy.trans_antisymmRel {α : Type u_1} [Preorder α] {a b c : α} (hab : a ⋖ b) (hbc : AntisymmRel (fun (x1 x2 : α) => x1 ≤ x2) b c) :
a ⋖ c
source
theorem covBy_congr_right {α : Type u_1} [Preorder α] {a b c : α} (hab : AntisymmRel (fun (x1 x2 : α) => x1 ≤ x2) a b) :
c ⋖ a ↔ c ⋖ b
source
instance instIsNonstrictStrictOrderWCovByCovBy {α : Type u_1} [Preorder α] :
IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 ⩿ x2) fun (x1 x2 : α) => x1 ⋖ x2
source
instance CovBy.isIrrefl {α : Type u_1} [Preorder α] :
IsIrrefl α fun (x1 x2 : α) => x1 ⋖ x2
source
theorem CovBy.Ioo_eq {α : Type u_1} [Preorder α] {a b : α} (h : a ⋖ b) :
Set.Ioo a b = ∅
source
theorem covBy_iff_Ioo_eq {α : Type u_1} [Preorder α] {a b : α} :
a ⋖ b ↔ a < b ∧ Set.Ioo a b = ∅
source
theorem CovBy.of_image {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a b : α} (f : α ↪o β) (h : f a ⋖ f b) :
a ⋖ b
source
theorem CovBy.image {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a b : α} (f : α ↪o β) (hab : a ⋖ b) (h : (Set.range ⇑f).OrdConnected) :
f a ⋖ f b
source
theorem Set.OrdConnected.apply_covBy_apply_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a b : α} (f : α ↪o β) (h : (range ⇑f).OrdConnected) :
f a ⋖ f b ↔ a ⋖ b
source
@[simp]
theorem apply_covBy_apply_iff {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a b : α} {E : Type u_3} [EquivLike E α β] [OrderIsoClass E α β] (e : E) :
e a ⋖ e b ↔ a ⋖ b
source
theorem covBy_of_eq_or_eq {α : Type u_1} [Preorder α] {a b : α} (hab : a < b) (h : ∀ (c : α), a ≤ c → c ≤ b → c = a ∨ c = b) :
a ⋖ b
source
@[deprecated CovBy.of_image (since := "2025-11-07")]
theorem OrderEmbedding.covBy_of_apply {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a b : α} (f : α ↪o β) (h : f a ⋖ f b) :
a ⋖ b

Alias of `CovBy.of_image`.

source
@[deprecated apply_covBy_apply_iff (since := "2025-11-07")]
theorem OrderIso.map_covBy {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {a b : α} {E : Type u_3} [EquivLike E α β] [OrderIsoClass E α β] (e : E) :
e a ⋖ e b ↔ a ⋖ b

Alias of `apply_covBy_apply_iff`.

source
theorem WCovBy.covBy_of_ne {α : Type u_1} [PartialOrder α] {a b : α} (h : a ⩿ b) (h2 : a ≠ b) :
a ⋖ b
source
theorem covBy_iff_wcovBy_and_ne {α : Type u_1} [PartialOrder α] {a b : α} :
a ⋖ b ↔ a ⩿ b ∧ a ≠ b
source
theorem wcovBy_iff_covBy_or_eq {α : Type u_1} [PartialOrder α] {a b : α} :
a ⩿ b ↔ a ⋖ b ∨ a = b
source
theorem wcovBy_iff_eq_or_covBy {α : Type u_1} [PartialOrder α] {a b : α} :
a ⩿ b ↔ a = b ∨ a ⋖ b
source
theorem WCovBy.covBy_or_eq {α : Type u_1} [PartialOrder α] {a b : α} :
a ⩿ b → a ⋖ b ∨ a = b

Alias of the forward direction of `wcovBy_iff_covBy_or_eq`.

source
theorem WCovBy.eq_or_covBy {α : Type u_1} [PartialOrder α] {a b : α} :
a ⩿ b → a = b ∨ a ⋖ b

Alias of the forward direction of `wcovBy_iff_eq_or_covBy`.

source
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
source
theorem covBy_iff_lt_and_eq_or_eq {α : Type u_1} [PartialOrder α] {a b : α} :
a ⋖ b ↔ a < b ∧ ∀ (c : α), a ≤ c → c ≤ b → c = a ∨ c = b

An `iff` version of `CovBy.eq_or_eq` and `covBy_of_eq_or_eq`.

source
theorem CovBy.Ico_eq {α : Type u_1} [PartialOrder α] {a b : α} (h : a ⋖ b) :
Set.Ico a b = {a}
source
theorem CovBy.Ioc_eq {α : Type u_1} [PartialOrder α] {a b : α} (h : a ⋖ b) :
Set.Ioc a b = {b}
source
theorem CovBy.Icc_eq {α : Type u_1} [PartialOrder α] {a b : α} (h : a ⋖ b) :
Set.Icc a b = {a, b}
source
theorem CovBy.Ioi_eq {α : Type u_1} [LinearOrder α] {a b : α} (h : a ⋖ b) :
Set.Ioi a = Set.Ici b
source
theorem CovBy.Iio_eq {α : Type u_1} [LinearOrder α] {a b : α} (h : a ⋖ b) :
Set.Iio b = Set.Iic a
source
theorem WCovBy.le_of_lt {α : Type u_1} [LinearOrder α] {a b c : α} (hab : a ⩿ b) (hcb : c < b) :
c ≤ a
source
theorem WCovBy.ge_of_gt {α : Type u_1} [LinearOrder α] {a b c : α} (hab : a ⩿ b) (hac : a < c) :
b ≤ c
source
theorem CovBy.le_of_lt {α : Type u_1} [LinearOrder α] {a b c : α} (hab : a ⋖ b) :
c < b → c ≤ a
source
theorem CovBy.ge_of_gt {α : Type u_1} [LinearOrder α] {a b c : α} (hab : a ⋖ b) :
a < c → b ≤ c
source
theorem CovBy.unique_left {α : Type u_1} [LinearOrder α] {a b c : α} (ha : a ⋖ c) (hb : b ⋖ c) :
a = b
source
theorem CovBy.unique_right {α : Type u_1} [LinearOrder α] {a b c : α} (hb : a ⋖ b) (hc : a ⋖ c) :
b = c
source
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`.

source
theorem covBy_iff_lt_iff_le_left {α : Type u_1} [LinearOrder α] {x y : α} :
x ⋖ y ↔ ∀ {z : α}, z < y ↔ z ≤ x
source
theorem covBy_iff_le_iff_lt_left {α : Type u_1} [LinearOrder α] {x y : α} :
x ⋖ y ↔ ∀ {z : α}, z ≤ x ↔ z < y
source
theorem covBy_iff_lt_iff_le_right {α : Type u_1} [LinearOrder α] {x y : α} :
x ⋖ y ↔ ∀ {z : α}, x < z ↔ y ≤ z
source
theorem covBy_iff_le_iff_lt_right {α : Type u_1} [LinearOrder α] {x y : α} :
x ⋖ y ↔ ∀ {z : α}, y ≤ z ↔ x < z
source
theorem CovBy.lt_iff_le_left {α : Type u_1} [LinearOrder α] {x y : α} :
x ⋖ y → ∀ {z : α}, z < y ↔ z ≤ x

Alias of the forward direction of `covBy_iff_lt_iff_le_left`.

source
theorem CovBy.le_iff_lt_left {α : Type u_1} [LinearOrder α] {x y : α} :
x ⋖ y → ∀ {z : α}, z ≤ x ↔ z < y

Alias of the forward direction of `covBy_iff_le_iff_lt_left`.

source
theorem CovBy.lt_iff_le_right {α : Type u_1} [LinearOrder α] {x y : α} :
x ⋖ y → ∀ {z : α}, x < z ↔ y ≤ z

Alias of the forward direction of `covBy_iff_lt_iff_le_right`.

source
theorem CovBy.le_iff_lt_right {α : Type u_1} [LinearOrder α] {x y : α} :
x ⋖ y → ∀ {z : α}, y ≤ z ↔ x < z

Alias of the forward direction of `covBy_iff_le_iff_lt_right`.

source
theorem LT.lt.exists_disjoint_Iio_Ioi {α : Type u_1} [LinearOrder α] {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'`.

source
@[simp]
theorem Bool.wcovBy_iff {a b : Bool} :
a ⩿ b ↔ a ≤ b
source
@[simp]
theorem Bool.covBy_iff {a b : Bool} :
a ⋖ b ↔ a < b
source
instance Bool.instDecidableRelWCovBy :
DecidableRel fun (x1 x2 : Bool) => x1 ⩿ x2
Equations

- x✝¹.instDecidableRelWCovBy x✝ = decidable_of_iff (x✝¹ ≤ x✝) ⋯

source
instance Bool.instDecidableRelCovBy :
DecidableRel fun (x1 x2 : Bool) => x1 ⋖ x2
Equations

- x✝¹.instDecidableRelCovBy x✝ = decidable_of_iff (x✝¹ < x✝) ⋯

source
@[simp]
theorem Set.wcovBy_insert {α : Type u_1} (x : α) (s : Set α) :
s ⩿ insert x s
source
@[simp]
theorem Set.sdiff_singleton_wcovBy {α : Type u_1} (s : Set α) (a : α) :
s \ {a} ⩿ s
source
@[simp]
theorem Set.covBy_insert {α : Type u_1} {s : Set α} {a : α} (ha : a ∉ s) :
s ⋖ insert a s
source
@[simp]
theorem Set.empty_covBy_singleton {α : Type u_1} (a : α) :
∅ ⋖ {a}
source
@[simp]
theorem Set.sdiff_singleton_covBy {α : Type u_1} {s : Set α} {a : α} (ha : a ∈ s) :
s \ {a} ⋖ s
source
theorem CovBy.exists_set_insert {α : Type u_1} {s t : Set α} (h : s ⋖ t) :
∃ a ∉ s, insert a s = t
source
theorem CovBy.exists_set_sdiff_singleton {α : Type u_1} {s t : Set α} (h : s ⋖ t) :
∃ a ∈ t, t \ {a} = s
source
theorem Set.covBy_iff_exists_insert {α : Type u_1} {s t : Set α} :
s ⋖ t ↔ ∃ a ∉ s, insert a s = t
source
theorem Set.covBy_iff_exists_sdiff_singleton {α : Type u_1} {s t : Set α} :
s ⋖ t ↔ ∃ a ∈ t, t \ {a} = s
source
theorem wcovBy_eq_reflGen_covBy {α : Type u_1} [PartialOrder α] :
(fun (x1 x2 : α) => x1 ⩿ x2) = Relation.ReflGen fun (x1 x2 : α) => x1 ⋖ x2
source
theorem transGen_wcovBy_eq_reflTransGen_covBy {α : Type u_1} [PartialOrder α] :
(Relation.TransGen fun (x1 x2 : α) => x1 ⩿ x2) = Relation.ReflTransGen fun (x1 x2 : α) => x1 ⋖ x2
source
theorem reflTransGen_wcovBy_eq_reflTransGen_covBy {α : Type u_1} [PartialOrder α] :
(Relation.ReflTransGen fun (x1 x2 : α) => x1 ⩿ x2) = Relation.ReflTransGen fun (x1 x2 : α) => x1 ⋖ x2
source
@[simp]
theorem Prod.swap_wcovBy_swap {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {x y : α × β} :
x.swap ⩿ y.swap ↔ x ⩿ y
source
@[simp]
theorem Prod.swap_covBy_swap {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {x y : α × β} :
x.swap ⋖ y.swap ↔ x ⋖ y
source
theorem Prod.fst_eq_or_snd_eq_of_wcovBy {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {x y : α × β} :
x ⩿ y → x.1 = y.1 ∨ x.2 = y.2
source
theorem WCovBy.fst {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {x y : α × β} (h : x ⩿ y) :
x.1 ⩿ y.1
source
theorem WCovBy.snd {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {x y : α × β} (h : x ⩿ y) :
x.2 ⩿ y.2
source
theorem Prod.mk_wcovBy_mk_iff_left {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {a₁ a₂ : α} {b : β} :
(a₁, b) ⩿ (a₂, b) ↔ a₁ ⩿ a₂
source
theorem Prod.mk_wcovBy_mk_iff_right {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {a : α} {b₁ b₂ : β} :
(a, b₁) ⩿ (a, b₂) ↔ b₁ ⩿ b₂
source
theorem Prod.mk_covBy_mk_iff_left {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {a₁ a₂ : α} {b : β} :
(a₁, b) ⋖ (a₂, b) ↔ a₁ ⋖ a₂
source
theorem Prod.mk_covBy_mk_iff_right {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {a : α} {b₁ b₂ : β} :
(a, b₁) ⋖ (a, b₂) ↔ b₁ ⋖ b₂
source
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₂
source
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₂
source
theorem Prod.wcovBy_iff {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {x y : α × β} :
x ⩿ y ↔ x.1 ⩿ y.1 ∧ x.2 = y.2 ∨ x.2 ⩿ y.2 ∧ x.1 = y.1
source
theorem Prod.covBy_iff {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {x y : α × β} :
x ⋖ y ↔ x.1 ⋖ y.1 ∧ x.2 = y.2 ∨ x.2 ⋖ y.2 ∧ x.1 = y.1
source
theorem WCovBy.eval {ι : Type u_3} {α : ι → Type u_4} [(i : ι) → Preorder (α i)] {a b : (i : ι) → α i} (h : a ⩿ b) (i : ι) :
a i ⩿ b i
source
theorem Pi.exists_forall_antisymmRel_of_covBy {ι : Type u_3} {α : ι → Type u_4} [(i : ι) → Preorder (α i)] {a b : (i : ι) → α i} (h : a ⋖ b) :
∃ (i : ι), ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) => x1 ≤ x2) (a j) (b j)
source
theorem Pi.exists_forall_antisymmRel_of_wcovBy {ι : Type u_3} {α : ι → Type u_4} [(i : ι) → Preorder (α i)] {a b : (i : ι) → α i} [Nonempty ι] (h : a ⩿ b) :
∃ (i : ι), ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) => x1 ≤ x2) (a j) (b j)
source
theorem Pi.wcovBy_iff_antisymmRel {ι : Type u_3} {α : ι → Type u_4} [(i : ι) → Preorder (α i)] {a b : (i : ι) → α i} [Nonempty ι] :
a ⩿ b ↔ ∃ (i : ι), a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) => x1 ≤ x2) (a j) (b j)

A characterisation of the `WCovBy` relation in products of preorders. See `Pi.wcovBy_iff` for the (more common) version in products of partial orders.

source
theorem Pi.covBy_iff_antisymmRel {ι : Type u_3} {α : ι → Type u_4} [(i : ι) → Preorder (α i)] {a b : (i : ι) → α i} :
a ⋖ b ↔ ∃ (i : ι), a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → AntisymmRel (fun (x1 x2 : α j) => x1 ≤ x2) (a j) (b j)

A characterisation of the `CovBy` relation in products of preorders. See `Pi.covBy_iff` for the (more common) version in products of partial orders.

source
theorem Pi.exists_forall_eq_of_covBy {ι : Type u_3} {α : ι → Type u_4} [(i : ι) → PartialOrder (α i)] {a b : (i : ι) → α i} (h : a ⋖ b) :
∃ (i : ι), ∀ (j : ι), j ≠ i → a j = b j
source
theorem Pi.exists_forall_eq_of_wcovBy {ι : Type u_3} {α : ι → Type u_4} [(i : ι) → PartialOrder (α i)] {a b : (i : ι) → α i} [Nonempty ι] (h : a ⩿ b) :
∃ (i : ι), ∀ (j : ι), j ≠ i → a j = b j
source
theorem Pi.wcovBy_iff {ι : Type u_3} {α : ι → Type u_4} [(i : ι) → PartialOrder (α i)] {a b : (i : ι) → α i} [Nonempty ι] :
a ⩿ b ↔ ∃ (i : ι), a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → a j = b j
source
theorem Pi.covBy_iff {ι : Type u_3} {α : ι → Type u_4} [(i : ι) → PartialOrder (α i)] {a b : (i : ι) → α i} :
a ⋖ b ↔ ∃ (i : ι), a i ⋖ b i ∧ ∀ (j : ι), j ≠ i → a j = b j
source
theorem Pi.wcovBy_iff_exists_right_eq {ι : Type u_3} {α : ι → Type u_4} [(i : ι) → PartialOrder (α i)] {a b : (i : ι) → α i} [Nonempty ι] [DecidableEq ι] :
a ⩿ b ↔ ∃ (i : ι) (x : α i), a i ⩿ x ∧ b = Function.update a i x
source
theorem Pi.covBy_iff_exists_right_eq {ι : Type u_3} {α : ι → Type u_4} [(i : ι) → PartialOrder (α i)] {a b : (i : ι) → α i} [DecidableEq ι] :
a ⋖ b ↔ ∃ (i : ι) (x : α i), a i ⋖ x ∧ b = Function.update a i x
source
theorem Pi.wcovBy_iff_exists_left_eq {ι : Type u_3} {α : ι → Type u_4} [(i : ι) → PartialOrder (α i)] {a b : (i : ι) → α i} [Nonempty ι] [DecidableEq ι] :
a ⩿ b ↔ ∃ (i : ι) (x : α i), x ⩿ b i ∧ a = Function.update b i x
source
theorem Pi.covBy_iff_exists_left_eq {ι : Type u_3} {α : ι → Type u_4} [(i : ι) → PartialOrder (α i)] {a b : (i : ι) → α i} [DecidableEq ι] :
a ⋖ b ↔ ∃ (i : ι) (x : α i), x ⋖ b i ∧ a = Function.update b i x
source
@[simp]
theorem WithTop.coe_wcovBy_coe {α : Type u_1} [Preorder α] {a b : α} :
↑a ⩿ ↑b ↔ a ⩿ b
source
@[simp]
theorem WithTop.coe_covBy_coe {α : Type u_1} [Preorder α] {a b : α} :
↑a ⋖ ↑b ↔ a ⋖ b
source
@[simp]
theorem WithTop.coe_covBy_top {α : Type u_1} [Preorder α] {a : α} :
↑a ⋖ ⊤ ↔ IsMax a
source
@[simp]
theorem WithTop.coe_wcovBy_top {α : Type u_1} [Preorder α] {a : α} :
↑a ⩿ ⊤ ↔ IsMax a
source
@[simp]
theorem WithBot.coe_wcovBy_coe {α : Type u_1} [Preorder α] {a b : α} :
↑a ⩿ ↑b ↔ a ⩿ b
source
@[simp]
theorem WithBot.coe_covBy_coe {α : Type u_1} [Preorder α] {a b : α} :
↑a ⋖ ↑b ↔ a ⋖ b
source
@[simp]
theorem WithBot.bot_covBy_coe {α : Type u_1} [Preorder α] {a : α} :
⊥ ⋖ ↑a ↔ IsMin a
source
@[simp]
theorem WithBot.bot_wcovBy_coe {α : Type u_1} [Preorder α] {a : α} :
⊥ ⩿ ↑a ↔ IsMin a
source
theorem exists_covBy_of_wellFoundedLT {α : Type u_1} [Preorder α] [wf : WellFoundedLT α] ⦃a : α⦄ (h : ¬IsMax a) :
∃ (a' : α), a ⋖ a'
source
theorem exists_covBy_of_wellFoundedGT {α : Type u_1} [Preorder α] [wf : WellFoundedGT α] ⦃a : α⦄ (h : ¬IsMin a) :
∃ (a' : α), a' ⋖ a