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} [Preorder α] (a : α) (b : α) : Prop

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

Equations

• (a ⩿ b) = (a ≤ b ∧ ∀ ⦃c : α⦄, a < c → ¬c < b)

def «term_⩿_» : Lean.TrailingParserDescr

Notation for Wcovby a b.

Equations

• «term_⩿_» = Lean.ParserDescr.trailingNode `term_⩿_ 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⩿ ") (Lean.ParserDescr.cat `term 51))

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 ≤ c → c ≤ b → c = 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

Equations

• @Wcovby.isRefl = @Wcovby.isRefl.proof_1

theorem Wcovby.Ioo_eq {α : Type u_1} [Preorder α] {a : α} {b : α} (h : a ⩿ b) : Set.Ioo 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 ⩿ b → ↑OrderDual.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 ⩿ a → ↑OrderDual.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 ≤ c → c ≤ b → c = 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 : α) : Prop

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

Equations

• (a ⋖ b) = (a < b ∧ ∀ ⦃c : α⦄, a < c → ¬c < b)

def «term_⋖_» : Lean.TrailingParserDescr

Notation for Covby a b.

Equations

• «term_⋖_» = Lean.ParserDescr.trailingNode `term_⋖_ 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋖ ") (Lean.ParserDescr.cat `term 51))

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 : α} [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 ⋖ b → ↑OrderDual.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 ⋖ a → ↑OrderDual.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

Equations

• @instIsNonstrictStrictOrderWcovbyCovbyToLT = @instIsNonstrictStrictOrderWcovbyCovbyToLT.proof_1

instance Covby.isIrrefl {α : Type u_1} [Preorder α] : IsIrrefl α fun x x_1 => x ⋖ x_1

Equations

• @Covby.isIrrefl = @Covby.isIrrefl.proof_1

theorem Covby.Ioo_eq {α : Type u_1} [Preorder α] {a : α} {b : α} (h : a ⋖ b) : Set.Ioo 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 ≤ c → c ≤ b → c = 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 ⩿ b → a ⋖ 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 ⩿ b → a = 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 ≤ c → c ≤ b → c = 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) : Set.Ioi a = Set.Ici b

theorem Covby.Iio_eq {α : Type u_1} [LinearOrder α] {a : α} {b : α} (h : a ⋖ b) : Set.Iio b = Set.Iic a

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 < b → c ≤ a

theorem Covby.ge_of_gt {α : Type u_1} [LinearOrder α] {a : α} {b : α} {c : α} (hab : a ⋖ b) : a < c → b ≤ 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

theorem reflTransGen_wcovby_eq_reflTransGen_covby {α : Type u_1} [PartialOrder α] : (Relation.ReflTransGen 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 : α × β} : Prod.swap x ⩿ Prod.swap y ↔ x ⩿ y

@[simp]

theorem Prod.swap_covby_swap {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {x : α × β} {y : α × β} : Prod.swap x ⋖ Prod.swap y ↔ x ⋖ y

theorem Prod.fst_eq_or_snd_eq_of_wcovby {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {x : α × β} {y : α × β} : x ⩿ y → x.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