doc-next-gen

Mathlib.Order.Cover

Module docstring

{"# 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. "}
WCovBy.le theorem
(h : a ⩿ b) : a ≤ b
Full source 
theorem WCovBy.le (h : a ⩿ b) : a ≤ b :=
  h.1
Weak Covering Implies Inequality
Informal description
If $b$ weakly covers $a$ (denoted $a \⩿ b$), then $a \leq b$.
WCovBy.refl theorem
(a : α) : a ⩿ a
Full source 
theorem WCovBy.refl (a : α) : a ⩿ a :=
  ⟨le_rfl, fun _ hc => hc.not_lt⟩
Reflexivity of Weak Covering Relation
Informal description
For any element $a$ in a preorder $\alpha$, $a$ weakly covers itself, i.e., $a \⩿ a$.
WCovBy.rfl theorem
: a ⩿ a
Full source 
@[simp] lemma WCovBy.rfl : a ⩿ a := WCovBy.refl a
Reflexivity of Weak Covering Relation
Informal description
For any element $a$ in a preorder, $a$ weakly covers itself, i.e., $a \⩿ a$.
Eq.wcovBy theorem
(h : a = b) : a ⩿ b
Full source 
protected theorem Eq.wcovBy (h : a = b) : a ⩿ b :=
  h ▸ WCovBy.rfl
Weak Covering Relation for Equal Elements
Informal description
For any elements $a$ and $b$ in a preorder, if $a = b$, then $b$ weakly covers $a$ (denoted $a \⩿ b$).
wcovBy_of_le_of_le theorem
(h1 : a ≤ b) (h2 : b ≤ a) : a ⩿ b
Full source 
theorem wcovBy_of_le_of_le (h1 : a ≤ b) (h2 : b ≤ a) : a ⩿ b :=
  ⟨h1, fun _ hac hcb => (hac.trans hcb).not_le h2⟩
Weak covering relation for equal elements in a preorder
Informal description
For any elements $a$ and $b$ in a preorder, if $a \leq b$ and $b \leq a$, then $b$ weakly covers $a$ (denoted $a \⩿ b$).
AntisymmRel.wcovBy theorem
(h : AntisymmRel (· ≤ ·) a b) : a ⩿ b
Full source 
theorem AntisymmRel.wcovBy (h : AntisymmRel (· ≤ ·) a b) : a ⩿ b :=
  wcovBy_of_le_of_le h.1 h.2
Weak covering relation for antisymmetric elements in a preorder
Informal description
For any elements $a$ and $b$ in a preorder, if $a \leq b$ and $b \leq a$ (i.e., they are related in both directions by the order relation), then $b$ weakly covers $a$ (denoted $a \⩿ b$).
WCovBy.wcovBy_iff_le theorem
(hab : a ⩿ b) : b ⩿ a ↔ b ≤ a
Full source 
theorem WCovBy.wcovBy_iff_le (hab : a ⩿ b) : b ⩿ ab ⩿ a ↔ b ≤ a :=
  ⟨fun h => h.le, fun h => h.wcovBy_of_le hab.le⟩
Weak Covering Symmetry Criterion: $b \⩿ a \leftrightarrow b \leq a$ under $a \⩿ b$
Informal description
For any elements $a$ and $b$ in a preorder such that $b$ weakly covers $a$ (denoted $a \⩿ b$), the statement that $a$ weakly covers $b$ (i.e., $b \⩿ a$) is equivalent to $b \leq a$.
wcovBy_of_eq_or_eq theorem
(hab : a ≤ b) (h : ∀ c, a ≤ c → c ≤ b → c = a ∨ c = b) : a ⩿ b
Full source 
theorem wcovBy_of_eq_or_eq (hab : a ≤ b) (h : ∀ c, a ≤ c → c ≤ b → c = a ∨ c = b) : a ⩿ b :=
  ⟨hab, fun c ha hb => (h c ha.le hb.le).elim ha.ne' hb.ne⟩
Weak Covering Criterion via Extremal Elements
Informal description
For any elements $a$ and $b$ in a preorder such that $a \leq b$, if for every element $c$ satisfying $a \leq c \leq b$ we have $c = a$ or $c = b$, then $b$ weakly covers $a$ (denoted $a \⩿ b$).
AntisymmRel.trans_wcovBy theorem
(hab : AntisymmRel (· ≤ ·) a b) (hbc : b ⩿ c) : a ⩿ c
Full source 
theorem AntisymmRel.trans_wcovBy (hab : AntisymmRel (· ≤ ·) a b) (hbc : b ⩿ c) : a ⩿ c :=
  ⟨hab.1.trans hbc.le, fun _ had hdc => hbc.2 (hab.2.trans_lt had) hdc⟩
Transitivity of Weak Covering under Antisymmetrization
Informal description
Let $a$, $b$, and $c$ be elements in a partially ordered set. If $a$ and $b$ are related by the antisymmetrization of the order relation (i.e., $a \leq b$ and $b \leq a$) and $b$ weakly covers $c$ (i.e., $b \leq c$ with no elements strictly between $b$ and $c$), then $a$ weakly covers $c$.
wcovBy_congr_left theorem
(hab : AntisymmRel (· ≤ ·) a b) : a ⩿ c ↔ b ⩿ c
Full source 
theorem wcovBy_congr_left (hab : AntisymmRel (· ≤ ·) a b) : a ⩿ ca ⩿ c ↔ b ⩿ c :=
  ⟨hab.symm.trans_wcovBy, hab.trans_wcovBy⟩
Weak Covering Relation is Congruent on the Left under Antisymmetric Equivalence
Informal description
For any elements $a$, $b$, and $c$ in a partially ordered set, if $a$ and $b$ are antisymmetrically related (i.e., $a \leq b$ and $b \leq a$), then $a$ weakly covers $c$ if and only if $b$ weakly covers $c$. In other words, the weak covering relation is preserved under antisymmetric equivalence on the left.
WCovBy.trans_antisymm_rel theorem
(hab : a ⩿ b) (hbc : AntisymmRel (· ≤ ·) b c) : a ⩿ c
Full source 
theorem WCovBy.trans_antisymm_rel (hab : a ⩿ b) (hbc : AntisymmRel (· ≤ ·) b c) : a ⩿ c :=
  ⟨hab.le.trans hbc.1, fun _ had hdc => hab.2 had <| hdc.trans_le hbc.2⟩
Transitivity of Weak Covering under Antisymmetric Relation
Informal description
Let $a$, $b$, and $c$ be elements in a partially ordered set. If $b$ weakly covers $a$ (denoted $a \⩿ b$) and $b$ and $c$ are antisymmetrically related (i.e., $b \leq c$ and $c \leq b$), then $c$ weakly covers $a$ (i.e., $a \⩿ c$).
wcovBy_congr_right theorem
(hab : AntisymmRel (· ≤ ·) a b) : c ⩿ a ↔ c ⩿ b
Full source 
theorem wcovBy_congr_right (hab : AntisymmRel (· ≤ ·) a b) : c ⩿ ac ⩿ a ↔ c ⩿ b :=
  ⟨fun h => h.trans_antisymm_rel hab, fun h => h.trans_antisymm_rel hab.symm⟩
Weak Covering Relation is Congruent on the Right under Antisymmetric Equivalence
Informal description
For any elements $a$, $b$, and $c$ in a partially ordered set, if $a$ and $b$ are antisymmetrically related (i.e., $a \leq b$ and $b \leq a$), then $c$ weakly covers $a$ if and only if $c$ weakly covers $b$. In other words, the weak covering relation is preserved under antisymmetric equivalence.
not_wcovBy_iff theorem
(h : a ≤ b) : ¬a ⩿ b ↔ ∃ c, a < c ∧ c < b
Full source 
/-- If `a ≤ b`, then `b` does not cover `a` iff there's an element in between. -/
theorem not_wcovBy_iff (h : a ≤ b) : ¬a ⩿ b¬a ⩿ b ↔ ∃ c, a < c ∧ c < b := by
  simp_rw [WCovBy, h, true_and, not_forall, exists_prop, not_not]
Characterization of Non-Weakly-Covering Elements via Intermediate Elements
Informal description
For elements $a$ and $b$ in a partially ordered set with $a \leq b$, the element $b$ does not weakly cover $a$ if and only if there exists an element $c$ such that $a < c < b$.
WCovBy.isRefl instance
: IsRefl α (· ⩿ ·)
Full source 
instance WCovBy.isRefl : IsRefl α (· ⩿ ·) :=
  ⟨WCovBy.refl⟩
Reflexivity of the Weak Covering Relation
Informal description
The weak covering relation $\⩿$ on a preorder $\alpha$ is reflexive, meaning that every element weakly covers itself.
WCovBy.Ioo_eq theorem
(h : a ⩿ b) : Ioo a b = ∅
Full source 
theorem WCovBy.Ioo_eq (h : a ⩿ b) : Ioo a b = ∅ :=
  eq_empty_iff_forall_not_mem.2 fun _ hx => h.2 hx.1 hx.2
Empty Interval under Weak Covering Relation: $a \ ⩿ \ b \Rightarrow (a, b) = \emptyset$
Informal description
For any elements $a$ and $b$ in a preorder, if $b$ weakly covers $a$ (denoted $a \ ⩿ \ b$), then the open interval $(a, b)$ is empty.
wcovBy_iff_Ioo_eq theorem
: a ⩿ b ↔ a ≤ b ∧ Ioo a b = ∅
Full source 
theorem wcovBy_iff_Ioo_eq : a ⩿ ba ⩿ b ↔ a ≤ b ∧ Ioo a b = ∅ :=
  and_congr_right' <| by simp [eq_empty_iff_forall_not_mem]
Characterization of Weak Covering Relation via Empty Interval: $a \ ⩿ \ b \leftrightarrow (a \leq b \land (a, b) = \emptyset)$
Informal description
For elements $a$ and $b$ in a preorder, $b$ weakly covers $a$ (denoted $a \ ⩿ \ b$) if and only if $a \leq b$ and the open interval $(a, b)$ is empty.
WCovBy.of_le_of_le theorem
(hac : a ⩿ c) (hab : a ≤ b) (hbc : b ≤ c) : b ⩿ c
Full source 
lemma WCovBy.of_le_of_le (hac : a ⩿ c) (hab : a ≤ b) (hbc : b ≤ c) : b ⩿ c :=
  ⟨hbc, fun _x hbx hxc ↦ hac.2 (hab.trans_lt hbx) hxc⟩
Weak Covering Relation is Preserved Under Intermediate Elements
Informal description
Let $a$, $b$, and $c$ be elements in a partially ordered set. If $a$ is weakly covered by $c$ (denoted $a \ ⩿ \ c$), and $a \leq b \leq c$, then $b$ is weakly covered by $c$ (denoted $b \ ⩿ \ c$).
WCovBy.of_le_of_le' theorem
(hac : a ⩿ c) (hab : a ≤ b) (hbc : b ≤ c) : a ⩿ b
Full source 
lemma WCovBy.of_le_of_le' (hac : a ⩿ c) (hab : a ≤ b) (hbc : b ≤ c) : a ⩿ b :=
  ⟨hab, fun _x hax hxb ↦ hac.2 hax <| hxb.trans_le hbc⟩
Weak covering relation under inequalities: \( a \ ⩿ \ b \) from \( a \leq b \leq c \) and \( a \ ⩿ \ c \)
Informal description
Let \( a, b, c \) be elements in a partially ordered set. If \( b \) weakly covers \( c \) (denoted \( a \ ⩿ \ c \)), and \( a \leq b \leq c \), then \( a \) weakly covers \( b \) (denoted \( a \ ⩿ \ b \)).
WCovBy.of_image theorem
(f : α ↪o β) (h : f a ⩿ f b) : a ⩿ b
Full source 
theorem WCovBy.of_image (f : α ↪o β) (h : f a ⩿ f b) : a ⩿ b :=
  ⟨f.le_iff_le.mp h.le, fun _ hac hcb => h.2 (f.lt_iff_lt.mpr hac) (f.lt_iff_lt.mpr hcb)⟩
Weak Covering Relation is Reflected by Order Embeddings
Informal description
Let $f \colon \alpha \hookrightarrow \beta$ be an order embedding between partially ordered sets. If $f(b)$ weakly covers $f(a)$ in $\beta$, then $b$ weakly covers $a$ in $\alpha$.
WCovBy.image theorem
(f : α ↪o β) (hab : a ⩿ b) (h : (range f).OrdConnected) : f a ⩿ f b
Full source 
theorem WCovBy.image (f : α ↪o β) (hab : a ⩿ b) (h : (range f).OrdConnected) : f a ⩿ f b := by
  refine ⟨f.monotone hab.le, fun c ha hb => ?_⟩
  obtain ⟨c, rfl⟩ := h.out (mem_range_self _) (mem_range_self _) ⟨ha.le, hb.le⟩
  rw [f.lt_iff_lt] at ha hb
  exact hab.2 ha hb
Order Embedding Preserves Weak Covering Relation on Order-Connected Range
Informal description
Let $f \colon \alpha \hookrightarrow \beta$ be an order embedding between partially ordered sets, and suppose the range of $f$ is order-connected. If $b$ weakly covers $a$ in $\alpha$ (denoted $a \⩿ b$), then $f(b)$ weakly covers $f(a)$ in $\beta$ (i.e., $f(a) \⩿ f(b)$).
Set.OrdConnected.apply_wcovBy_apply_iff theorem
(f : α ↪o β) (h : (range f).OrdConnected) : f a ⩿ f b ↔ a ⩿ b
Full source 
theorem Set.OrdConnected.apply_wcovBy_apply_iff (f : α ↪o β) (h : (range f).OrdConnected) :
    f a ⩿ f bf a ⩿ f b ↔ a ⩿ b :=
  ⟨fun h2 => h2.of_image f, fun hab => hab.image f h⟩
Equivalence of Weak Covering Relations Under Order Embedding with Order-Connected Range
Informal description
Let $f \colon \alpha \hookrightarrow \beta$ be an order embedding between partially ordered sets, and suppose the range of $f$ is order-connected. Then for any elements $a, b \in \alpha$, the weakly covering relation $f(a) \⩿ f(b)$ holds in $\beta$ if and only if $a \⩿ b$ holds in $\alpha$.
apply_wcovBy_apply_iff theorem
{E : Type*} [EquivLike E α β] [OrderIsoClass E α β] (e : E) : e a ⩿ e b ↔ a ⩿ b
Full source 
@[simp]
theorem apply_wcovBy_apply_iff {E : Type*} [EquivLike E α β] [OrderIsoClass E α β] (e : E) :
    e a ⩿ e be a ⩿ e b ↔ a ⩿ b :=
  (ordConnected_range (e : α ≃o β)).apply_wcovBy_apply_iff ((e : α ≃o β) : α ↪o β)
Order Isomorphism Preserves Weak Covering Relation: $e(a) \⩿ e(b) \leftrightarrow a \⩿ b$
Informal description
Let $\alpha$ and $\beta$ be preordered sets, and let $E$ be a type of order-preserving bijections between them (order isomorphisms). For any order isomorphism $e \in E$ and elements $a, b \in \alpha$, the weakly covering relation $e(a) \⩿ e(b)$ holds in $\beta$ if and only if $a \⩿ b$ holds in $\alpha$.
toDual_wcovBy_toDual_iff theorem
: toDual b ⩿ toDual a ↔ a ⩿ b
Full source 
@[simp]
theorem toDual_wcovBy_toDual_iff : toDualtoDual b ⩿ toDual atoDual b ⩿ toDual a ↔ a ⩿ b :=
  and_congr_right' <| forall_congr' fun _ => forall_swap
Weak Covering Relation in Order Dual: $\operatorname{toDual}(b) \ ⩿ \ \operatorname{toDual}(a) \leftrightarrow a \ ⩿ \ b$
Informal description
For any elements $a$ and $b$ in a preorder $\alpha$, the weakly covering relation holds between the order dual elements $\operatorname{toDual}(b)$ and $\operatorname{toDual}(a)$ if and only if $a$ weakly covers $b$ in the original order. In other words, $\operatorname{toDual}(b) \ ⩿ \ \operatorname{toDual}(a) \leftrightarrow a \ ⩿ \ b$.
ofDual_wcovBy_ofDual_iff theorem
{a b : αᵒᵈ} : ofDual a ⩿ ofDual b ↔ b ⩿ a
Full source 
@[simp]
theorem ofDual_wcovBy_ofDual_iff {a b : αᵒᵈ} : ofDualofDual a ⩿ ofDual bofDual a ⩿ ofDual b ↔ b ⩿ a :=
  and_congr_right' <| forall_congr' fun _ => forall_swap
Weak Covering Relation in Order Dual via ofDual: $\operatorname{ofDual}(a) \ ⩿ \ \operatorname{ofDual}(b) \leftrightarrow b \ ⩿ \ a$
Informal description
For any elements $a$ and $b$ in the order dual $\alpha^{\text{op}}$ of a preorder $\alpha$, the weakly covering relation holds between $\operatorname{ofDual}(a)$ and $\operatorname{ofDual}(b)$ if and only if $b$ weakly covers $a$ in the original order. In other words, $\operatorname{ofDual}(a) \ ⩿ \ \operatorname{ofDual}(b) \leftrightarrow b \ ⩿ \ a$.
OrderEmbedding.wcovBy_of_apply theorem
{α β : Type*} [Preorder α] [Preorder β] (f : α ↪o β) {x y : α} (h : f x ⩿ f y) : x ⩿ y
Full source 
theorem OrderEmbedding.wcovBy_of_apply {α β : Type*} [Preorder α] [Preorder β]
    (f : α ↪o β) {x y : α} (h : f x ⩿ f y) : x ⩿ y := by
  use f.le_iff_le.1 h.1
  intro a
  rw [← f.lt_iff_lt, ← f.lt_iff_lt]
  apply h.2
Order Embedding Preserves Weak Covering Relation: $f(x) \ ⩿ \ f(y) \to x \ ⩿ \ y$
Informal description
Let $\alpha$ and $\beta$ be preordered types, and let $f \colon \alpha \hookrightarrow \beta$ be an order embedding. For any elements $x, y \in \alpha$, if $f(x)$ weakly covers $f(y)$ in $\beta$ (i.e., $f(x) \ ⩿ \ f(y)$), then $x$ weakly covers $y$ in $\alpha$ (i.e., $x \ ⩿ \ y$).
OrderIso.map_wcovBy theorem
{α β : Type*} [Preorder α] [Preorder β] (f : α ≃o β) {x y : α} : f x ⩿ f y ↔ x ⩿ y
Full source 
theorem OrderIso.map_wcovBy {α β : Type*} [Preorder α] [Preorder β]
    (f : α ≃o β) {x y : α} : f x ⩿ f yf x ⩿ f y ↔ x ⩿ y := by
  use f.toOrderEmbedding.wcovBy_of_apply
  conv_lhs => rw [← f.symm_apply_apply x, ← f.symm_apply_apply y]
  exact f.symm.toOrderEmbedding.wcovBy_of_apply
Order Isomorphism Preserves Weak Covering Relation: $f(x) \ ⩿ \ f(y) \leftrightarrow x \ ⩿ \ y$
Informal description
Let $\alpha$ and $\beta$ be preordered types, and let $f \colon \alpha \simeq_o \beta$ be an order isomorphism. For any elements $x, y \in \alpha$, the weakly covering relation holds between their images under $f$ if and only if it holds between $x$ and $y$ in $\alpha$, i.e., $f(x) \ ⩿ \ f(y) \leftrightarrow x \ ⩿ \ y$.
wcovBy_iff_le_and_eq_or_eq theorem
: a ⩿ b ↔ a ≤ b ∧ ∀ c, a ≤ c → c ≤ b → c = a ∨ c = b
Full source 
/-- An `iff` version of `WCovBy.eq_or_eq` and `wcovBy_of_eq_or_eq`. -/
theorem wcovBy_iff_le_and_eq_or_eq : a ⩿ ba ⩿ b ↔ a ≤ b ∧ ∀ c, a ≤ c → c ≤ b → c = a ∨ c = b :=
  ⟨fun h => ⟨h.le, fun _ => h.eq_or_eq⟩, And.rec wcovBy_of_eq_or_eq⟩
Characterization of Weak Covering via Extremal Elements
Informal description
For elements $a$ and $b$ in a preorder, $b$ weakly covers $a$ (denoted $a \⩿ b$) if and only if $a \leq b$ and for every element $c$ satisfying $a \leq c \leq b$, we have $c = a$ or $c = b$.
WCovBy.le_and_le_iff theorem
(h : a ⩿ b) : a ≤ c ∧ c ≤ b ↔ c = a ∨ c = b
Full source 
theorem WCovBy.le_and_le_iff (h : a ⩿ b) : a ≤ c ∧ c ≤ ba ≤ c ∧ c ≤ b ↔ c = a ∨ c = b := by
  refine ⟨fun h2 => h.eq_or_eq h2.1 h2.2, ?_⟩; rintro (rfl | rfl)
  exacts [⟨le_rfl, h.le⟩, ⟨h.le, le_rfl⟩]
Characterization of Elements Between Weakly Covering Pair
Informal description
Let $a$ and $b$ be elements in a partially ordered set such that $b$ weakly covers $a$ (denoted $a \⩿ b$). Then for any element $c$, the condition $a \leq c \leq b$ holds if and only if $c = a$ or $c = b$.
WCovBy.Icc_eq theorem
(h : a ⩿ b) : Icc a b = { a, b }
Full source 
theorem WCovBy.Icc_eq (h : a ⩿ b) : Icc a b = {a, b} := by
  ext c
  exact h.le_and_le_iff
Closed Interval Characterization for Weakly Covering Elements: $[a, b] = \{a, b\}$ when $a \⩿ b$
Informal description
Let $a$ and $b$ be elements in a preorder such that $b$ weakly covers $a$ (denoted $a \⩿ b$). Then the closed interval $[a, b]$ is equal to the two-element set $\{a, b\}$.
WCovBy.Ico_subset theorem
(h : a ⩿ b) : Ico a b ⊆ { a }
Full source 
theorem WCovBy.Ico_subset (h : a ⩿ b) : IcoIco a b ⊆ {a} := by
  rw [← Icc_diff_right, h.Icc_eq, diff_singleton_subset_iff, pair_comm]
Left-closed right-open interval characterization for weakly covering elements: $[a, b) \subseteq \{a\}$ when $a \⩿ b$
Informal description
Let $a$ and $b$ be elements in a preorder such that $b$ weakly covers $a$ (denoted $a \⩿ b$). Then the left-closed right-open interval $[a, b)$ is a subset of the singleton set $\{a\}$.
WCovBy.Ioc_subset theorem
(h : a ⩿ b) : Ioc a b ⊆ { b }
Full source 
theorem WCovBy.Ioc_subset (h : a ⩿ b) : IocIoc a b ⊆ {b} := by
  rw [← Icc_diff_left, h.Icc_eq, diff_singleton_subset_iff]
Weakly Covered Interval Subset: $(a, b] \subseteq \{b\}$ when $a \⩿ b$
Informal description
Let $a$ and $b$ be elements in a preorder such that $b$ weakly covers $a$ (denoted $a \⩿ b$). Then the left-open right-closed interval $(a, b]$ is a subset of the singleton set $\{b\}$.
WCovBy.sup_eq theorem
(hac : a ⩿ c) (hbc : b ⩿ c) (hab : a ≠ b) : a ⊔ b = c
Full source 
theorem WCovBy.sup_eq (hac : a ⩿ c) (hbc : b ⩿ c) (hab : a ≠ b) : a ⊔ b = c :=
  (sup_le hac.le hbc.le).eq_of_not_lt fun h =>
    hab.lt_sup_or_lt_sup.elim (fun h' => hac.2 h' h) fun h' => hbc.2 h' h
Supremum of Weakly Covered Elements in Join-Semilattice
Informal description
Let $a$, $b$, and $c$ be elements in a join-semilattice such that: 1. $c$ weakly covers $a$ (denoted $a \⩿ c$), 2. $c$ weakly covers $b$ (denoted $b \⩿ c$), and 3. $a \neq b$. Then the supremum of $a$ and $b$ equals $c$, i.e., $a \sqcup b = c$.
WCovBy.inf_eq theorem
(hca : c ⩿ a) (hcb : c ⩿ b) (hab : a ≠ b) : a ⊓ b = c
Full source 
theorem WCovBy.inf_eq (hca : c ⩿ a) (hcb : c ⩿ b) (hab : a ≠ b) : a ⊓ b = c :=
  (le_inf hca.le hcb.le).eq_of_not_gt fun h => hab.inf_lt_or_inf_lt.elim (hca.2 h) (hcb.2 h)
Infimum of Weakly Covered Elements in Meet-Semilattice
Informal description
Let $a$, $b$, and $c$ be elements in a meet-semilattice such that: 1. $a$ weakly covers $c$ (denoted $c \⩿ a$), 2. $b$ weakly covers $c$ (denoted $c \⩿ b$), and 3. $a \neq b$. Then the infimum of $a$ and $b$ equals $c$, i.e., $a \sqcap b = c$.
CovBy.lt theorem
(h : a ⋖ b) : a < b
Full source 
theorem CovBy.lt (h : a ⋖ b) : a < b :=
  h.1
Covering relation implies strict inequality
Informal description
If $b$ covers $a$ (denoted $a \lessdot b$), then $a$ is strictly less than $b$, i.e., $a < b$.
not_covBy_iff theorem
(h : a < b) : ¬a ⋖ b ↔ ∃ c, a < c ∧ c < b
Full source 
/-- If `a < b`, then `b` does not cover `a` iff there's an element in between. -/
theorem not_covBy_iff (h : a < b) : ¬a ⋖ b¬a ⋖ b ↔ ∃ c, a < c ∧ c < b := by
  simp_rw [CovBy, h, true_and, not_forall, exists_prop, not_not]
Characterization of Non-Covering Relation via Intermediate Elements
Informal description
For elements $a$ and $b$ in a partially ordered set with $a < b$, the element $b$ does not cover $a$ if and only if there exists an element $c$ such that $a < c < b$.
not_covBy theorem
[DenselyOrdered α] : ¬a ⋖ b
Full source 
/-- In a dense order, nothing covers anything. -/
theorem not_covBy [DenselyOrdered α] : ¬a ⋖ b := fun h =>
  let ⟨_, hc⟩ := exists_between h.1
  h.2 hc.1 hc.2
Absence of Covering Relations in Dense Orders
Informal description
In a densely ordered set $\alpha$, there are no covering relations, i.e., for any elements $a, b \in \alpha$, it is not the case that $b$ covers $a$ (denoted $a \lessdot b$).
denselyOrdered_iff_forall_not_covBy theorem
: DenselyOrdered α ↔ ∀ a b : α, ¬a ⋖ b
Full source 
theorem denselyOrdered_iff_forall_not_covBy : DenselyOrderedDenselyOrdered α ↔ ∀ a b : α, ¬a ⋖ b :=
  ⟨fun h _ _ => @not_covBy _ _ _ _ h, fun h =>
    ⟨fun _ _ hab => exists_lt_lt_of_not_covBy hab <| h _ _⟩⟩
Dense Order Characterization via Absence of Covering Relations
Informal description
An order on a type $\alpha$ is dense if and only if there are no covering relations between any two elements $a$ and $b$ in $\alpha$, i.e., $\alpha$ is densely ordered if and only if for all $a, b \in \alpha$, it is not the case that $b$ covers $a$ (denoted $a \lessdot b$).
toDual_covBy_toDual_iff theorem
: toDual b ⋖ toDual a ↔ a ⋖ b
Full source 
@[simp]
theorem toDual_covBy_toDual_iff : toDualtoDual b ⋖ toDual atoDual b ⋖ toDual a ↔ a ⋖ b :=
  and_congr_right' <| forall_congr' fun _ => forall_swap
Covering Relation in Order Dual ↔ Original Covering Relation
Informal description
For any elements $a$ and $b$ in a partially ordered set $\alpha$, the order dual element $\text{toDual}(b)$ covers $\text{toDual}(a)$ in the order dual $\alpha^{\text{op}}$ if and only if $a$ covers $b$ in the original order $\alpha$. In other words, $\text{toDual}(b) \lessdot \text{toDual}(a) \leftrightarrow a \lessdot b$.
ofDual_covBy_ofDual_iff theorem
{a b : αᵒᵈ} : ofDual a ⋖ ofDual b ↔ b ⋖ a
Full source 
@[simp]
theorem ofDual_covBy_ofDual_iff {a b : αᵒᵈ} : ofDualofDual a ⋖ ofDual bofDual a ⋖ ofDual b ↔ b ⋖ a :=
  and_congr_right' <| forall_congr' fun _ => forall_swap
Covering Relation Duality: $\text{ofDual}(a) \lessdot \text{ofDual}(b) \leftrightarrow b \lessdot a$
Informal description
For any elements $a$ and $b$ in the order dual $\alpha^{\text{op}}$, the element $\text{ofDual}(a)$ covers $\text{ofDual}(b)$ in the original order $\alpha$ if and only if $b$ covers $a$ in the order dual $\alpha^{\text{op}}$. In other words, $\text{ofDual}(a) \lessdot \text{ofDual}(b) \leftrightarrow b \lessdot a$.
CovBy.le theorem
(h : a ⋖ b) : a ≤ b
Full source 
theorem CovBy.le (h : a ⋖ b) : a ≤ b :=
  h.1.le
Covering Implies Weak Ordering
Informal description
If $b$ covers $a$ (denoted $a \lessdot b$), then $a \leq b$.
CovBy.ne theorem
(h : a ⋖ b) : a ≠ b
Full source 
protected theorem CovBy.ne (h : a ⋖ b) : a ≠ b :=
  h.lt.ne
Covering relation implies inequality ($a \lessdot b \Rightarrow a \neq b$)
Informal description
If $b$ covers $a$ (denoted $a \lessdot b$), then $a$ is not equal to $b$.
CovBy.ne' theorem
(h : a ⋖ b) : b ≠ a
Full source 
theorem CovBy.ne' (h : a ⋖ b) : b ≠ a :=
  h.lt.ne'
Covering relation implies inequality ($a \lessdot b \Rightarrow b \neq a$)
Informal description
If $b$ covers $a$ (denoted $a \lessdot b$), then $b$ is not equal to $a$, i.e., $b \neq a$.
CovBy.wcovBy theorem
(h : a ⋖ b) : a ⩿ b
Full source 
protected theorem CovBy.wcovBy (h : a ⋖ b) : a ⩿ b :=
  ⟨h.le, h.2⟩
Covering Implies Weak Covering
Informal description
If $b$ covers $a$ (denoted $a \lessdot b$), then $b$ weakly covers $a$ (denoted $a \⩿ b$).
WCovBy.covBy_of_not_le theorem
(h : a ⩿ b) (h2 : ¬b ≤ a) : a ⋖ b
Full source 
theorem WCovBy.covBy_of_not_le (h : a ⩿ b) (h2 : ¬b ≤ a) : a ⋖ b :=
  ⟨h.le.lt_of_not_le h2, h.2⟩
Weak covering implies covering when not symmetric ($a \⩿ b$ and $\neg(b \leq a)$ implies $a \⋖ b$)
Informal description
If $b$ weakly covers $a$ (denoted $a \⩿ b$) and it is not the case that $b \leq a$, then $b$ covers $a$ (denoted $a \⋖ b$).
WCovBy.covBy_of_lt theorem
(h : a ⩿ b) (h2 : a < b) : a ⋖ b
Full source 
theorem WCovBy.covBy_of_lt (h : a ⩿ b) (h2 : a < b) : a ⋖ b :=
  ⟨h2, h.2⟩
Weak covering relation implies covering relation under strict inequality
Informal description
If $b$ weakly covers $a$ (denoted $a ⩿ b$) and $a < b$, then $b$ covers $a$ (denoted $a ⋖ b$).
CovBy.of_lt_of_le theorem
(hac : a ⋖ c) (hab : a < b) (hbc : b ≤ c) : a ⋖ b
Full source 
lemma CovBy.of_lt_of_le (hac : a ⋖ c) (hab : a < b) (hbc : b ≤ c) : a ⋖ b :=
  ⟨hab, fun _x hax hxb ↦ hac.2 hax <| hxb.trans_le hbc⟩
Covering relation under left strict and right non-strict inequality
Informal description
Let $a$, $b$, and $c$ be elements in a partially ordered set. If $c$ covers $a$ (denoted $a \lessdot c$), $a < b$, and $b \leq c$, then $b$ covers $a$ (i.e., $a \lessdot b$).
not_covBy_of_lt_of_lt theorem
(h₁ : a < b) (h₂ : b < c) : ¬a ⋖ c
Full source 
theorem not_covBy_of_lt_of_lt (h₁ : a < b) (h₂ : b < c) : ¬a ⋖ c :=
  (not_covBy_iff (h₁.trans h₂)).2 ⟨b, h₁, h₂⟩
No Covering Relation Between Elements with Intermediate Element
Informal description
For elements $a$, $b$, and $c$ in a partially ordered set, if $a < b$ and $b < c$, then $c$ does not cover $a$.
covBy_iff_wcovBy_and_not_le theorem
: a ⋖ b ↔ a ⩿ b ∧ ¬b ≤ a
Full source 
theorem covBy_iff_wcovBy_and_not_le : a ⋖ ba ⋖ b ↔ a ⩿ b ∧ ¬b ≤ a :=
  ⟨fun h => ⟨h.wcovBy, h.lt.not_le⟩, fun h => h.1.covBy_of_not_le h.2⟩
Characterization of Covering Relation: $a \lessdot b \leftrightarrow (a \⩿ b \land \neg(b \leq a))$
Informal description
For elements $a$ and $b$ in a partially ordered set, $b$ covers $a$ (denoted $a \lessdot b$) if and only if $b$ weakly covers $a$ (denoted $a \⩿ b$) and it is not the case that $b \leq a$.
wcovBy_iff_covBy_or_le_and_le theorem
: a ⩿ b ↔ a ⋖ b ∨ a ≤ b ∧ b ≤ a
Full source 
theorem wcovBy_iff_covBy_or_le_and_le : a ⩿ ba ⩿ b ↔ a ⋖ b ∨ a ≤ b ∧ b ≤ a :=
  ⟨fun h => or_iff_not_imp_right.mpr fun h' => h.covBy_of_not_le fun hba => h' ⟨h.le, hba⟩,
    fun h' => h'.elim (fun h => h.wcovBy) fun h => h.1.wcovBy_of_le h.2⟩
Characterization of Weak Covering: $a \⩿ b \leftrightarrow (a \⋖ b \lor (a \leq b \land b \leq a))$
Informal description
For any elements $a$ and $b$ in a partially ordered set, $b$ weakly covers $a$ (denoted $a \⩿ b$) if and only if either $b$ covers $a$ (denoted $a \⋖ b$) or both $a \leq b$ and $b \leq a$ hold.
AntisymmRel.trans_covBy theorem
(hab : AntisymmRel (· ≤ ·) a b) (hbc : b ⋖ c) : a ⋖ c
Full source 
theorem AntisymmRel.trans_covBy (hab : AntisymmRel (· ≤ ·) a b) (hbc : b ⋖ c) : a ⋖ c :=
  ⟨hab.1.trans_lt hbc.lt, fun _ had hdc => hbc.2 (hab.2.trans_lt had) hdc⟩
Transitivity of Covering Relation under Antisymmetrization
Informal description
Let $a$, $b$, and $c$ be elements in a partially ordered set. If $a$ and $b$ are related by the antisymmetrization of the order relation (i.e., $a \leq b$ and $b \leq a$), and $b$ is covered by $c$ (i.e., $b \lessdot c$), then $a$ is also covered by $c$ (i.e., $a \lessdot c$).
covBy_congr_left theorem
(hab : AntisymmRel (· ≤ ·) a b) : a ⋖ c ↔ b ⋖ c
Full source 
theorem covBy_congr_left (hab : AntisymmRel (· ≤ ·) a b) : a ⋖ ca ⋖ c ↔ b ⋖ c :=
  ⟨hab.symm.trans_covBy, hab.trans_covBy⟩
Covering Relation Congruence under Antisymmetrization on the Left
Informal description
Let $a$, $b$, and $c$ be elements in a partially ordered set. If $a$ and $b$ are related by the antisymmetrization of the order relation (i.e., $a \leq b$ and $b \leq a$), then $a$ is covered by $c$ (i.e., $a \lessdot c$) if and only if $b$ is covered by $c$ (i.e., $b \lessdot c$).
CovBy.trans_antisymmRel theorem
(hab : a ⋖ b) (hbc : AntisymmRel (· ≤ ·) b c) : a ⋖ c
Full source 
theorem CovBy.trans_antisymmRel (hab : a ⋖ b) (hbc : AntisymmRel (· ≤ ·) b c) : a ⋖ c :=
  ⟨hab.lt.trans_le hbc.1, fun _ had hdb => hab.2 had <| hdb.trans_le hbc.2⟩
Transitivity of Covering Relation with Antisymmetric Elements
Informal description
If $b$ covers $a$ (denoted $a \lessdot b$) and $b$ is antisymmetrically related to $c$ (i.e., $b \leq c$ and $c \leq b$), then $c$ covers $a$ (i.e., $a \lessdot c$).
covBy_congr_right theorem
(hab : AntisymmRel (· ≤ ·) a b) : c ⋖ a ↔ c ⋖ b
Full source 
theorem covBy_congr_right (hab : AntisymmRel (· ≤ ·) a b) : c ⋖ ac ⋖ a ↔ c ⋖ b :=
  ⟨fun h => h.trans_antisymmRel hab, fun h => h.trans_antisymmRel hab.symm⟩
Covering Relation Congruence under Antisymmetrization on the Right
Informal description
For any elements $a$, $b$, and $c$ in a partially ordered set, if $a$ and $b$ are antisymmetrically related (i.e., $a \leq b$ and $b \leq a$), then $c$ covers $a$ (denoted $c \lessdot a$) if and only if $c$ covers $b$ (denoted $c \lessdot b$).
instIsNonstrictStrictOrderWCovByCovBy instance
: IsNonstrictStrictOrder α (· ⩿ ·) (· ⋖ ·)
Full source 
instance : IsNonstrictStrictOrder α (· ⩿ ·) (· ⋖ ·) :=
  ⟨fun _ _ =>
    covBy_iff_wcovBy_and_not_le.trans <| and_congr_right fun h => h.wcovBy_iff_le.not.symm⟩
Weak Covering and Covering as Nonstrict-Strict Order Pair
Informal description
The weak covering relation $\⩿$ and the covering relation $\lessdot$ on a type $\alpha$ form a nonstrict-strict order pair, meaning that for any elements $a$ and $b$ in $\alpha$, $a \lessdot b$ holds if and only if $a \⩿ b$ holds and $b \⩿ a$ does not hold.
CovBy.isIrrefl instance
: IsIrrefl α (· ⋖ ·)
Full source 
instance CovBy.isIrrefl : IsIrrefl α (· ⋖ ·) :=
  ⟨fun _ ha => ha.ne rfl⟩
Irreflexivity of the Covering Relation
Informal description
The covering relation $\lessdot$ on a type $\alpha$ is irreflexive, meaning that for any element $a \in \alpha$, $a \lessdot a$ does not hold.
CovBy.Ioo_eq theorem
(h : a ⋖ b) : Ioo a b = ∅
Full source 
theorem CovBy.Ioo_eq (h : a ⋖ b) : Ioo a b = ∅ :=
  h.wcovBy.Ioo_eq
Empty Interval under Covering Relation: $a \lessdot b \Rightarrow (a, b) = \emptyset$
Informal description
If $b$ covers $a$ (denoted $a \lessdot b$) in a preorder, then the open interval $(a, b)$ is empty, i.e., $\text{Ioo}(a, b) = \emptyset$.
covBy_iff_Ioo_eq theorem
: a ⋖ b ↔ a < b ∧ Ioo a b = ∅
Full source 
theorem covBy_iff_Ioo_eq : a ⋖ ba ⋖ b ↔ a < b ∧ Ioo a b = ∅ :=
  and_congr_right' <| by simp [eq_empty_iff_forall_not_mem]
Characterization of Covering Relation via Empty Interval: $a \lessdot b \leftrightarrow a < b \land (a, b) = \emptyset$
Informal description
For any two elements $a$ and $b$ in a preorder, $b$ covers $a$ (denoted $a \lessdot b$) if and only if $a < b$ and the open interval $(a, b)$ is empty.
CovBy.of_image theorem
(f : α ↪o β) (h : f a ⋖ f b) : a ⋖ b
Full source 
theorem CovBy.of_image (f : α ↪o β) (h : f a ⋖ f b) : a ⋖ b :=
  ⟨f.lt_iff_lt.mp h.lt, fun _ hac hcb => h.2 (f.lt_iff_lt.mpr hac) (f.lt_iff_lt.mpr hcb)⟩
Covering Relation Preserved by Order Embedding Inverses: $f(a) \lessdot f(b) \Rightarrow a \lessdot b$
Informal description
Let $f \colon \alpha \hookrightarrow \beta$ be an order embedding between preordered types. If $f(b)$ covers $f(a)$ in $\beta$ (i.e., $f(a) \lessdot f(b)$), then $b$ covers $a$ in $\alpha$ (i.e., $a \lessdot b$).
CovBy.image theorem
(f : α ↪o β) (hab : a ⋖ b) (h : (range f).OrdConnected) : f a ⋖ f b
Full source 
theorem CovBy.image (f : α ↪o β) (hab : a ⋖ b) (h : (range f).OrdConnected) : f a ⋖ f b :=
  (hab.wcovBy.image f h).covBy_of_lt <| f.strictMono hab.lt
Order Embedding Preserves Covering Relation on Order-Connected Range
Informal description
Let $f \colon \alpha \hookrightarrow \beta$ be an order embedding between partially ordered sets, and suppose the range of $f$ is order-connected. If $b$ covers $a$ in $\alpha$ (denoted $a \lessdot b$), then $f(b)$ covers $f(a)$ in $\beta$ (i.e., $f(a) \lessdot f(b)$).
Set.OrdConnected.apply_covBy_apply_iff theorem
(f : α ↪o β) (h : (range f).OrdConnected) : f a ⋖ f b ↔ a ⋖ b
Full source 
theorem Set.OrdConnected.apply_covBy_apply_iff (f : α ↪o β) (h : (range f).OrdConnected) :
    f a ⋖ f bf a ⋖ f b ↔ a ⋖ b :=
  ⟨CovBy.of_image f, fun hab => hab.image f h⟩
Order-Embedding Characterization of Covering Relation on Order-Connected Range: $f(a) \lessdot f(b) \leftrightarrow a \lessdot b$
Informal description
Let $f \colon \alpha \hookrightarrow \beta$ be an order embedding between preordered sets, and suppose the range of $f$ is order-connected. Then for any elements $a, b \in \alpha$, the image $f(b)$ covers $f(a)$ in $\beta$ (denoted $f(a) \lessdot f(b)$) if and only if $b$ covers $a$ in $\alpha$ (denoted $a \lessdot b$).
apply_covBy_apply_iff theorem
{E : Type*} [EquivLike E α β] [OrderIsoClass E α β] (e : E) : e a ⋖ e b ↔ a ⋖ b
Full source 
@[simp]
theorem apply_covBy_apply_iff {E : Type*} [EquivLike E α β] [OrderIsoClass E α β] (e : E) :
    e a ⋖ e be a ⋖ e b ↔ a ⋖ b :=
  (ordConnected_range (e : α ≃o β)).apply_covBy_apply_iff ((e : α ≃o β) : α ↪o β)
Order Isomorphism Preserves Covering Relation: $e(a) \lessdot e(b) \leftrightarrow a \lessdot b$
Informal description
Let $\alpha$ and $\beta$ be preordered types, and let $E$ be a type of order isomorphisms between $\alpha$ and $\beta$. For any order isomorphism $e \in E$ and elements $a, b \in \alpha$, the image $e(b)$ covers $e(a)$ in $\beta$ (denoted $e(a) \lessdot e(b)$) if and only if $b$ covers $a$ in $\alpha$ (denoted $a \lessdot b$).
covBy_of_eq_or_eq theorem
(hab : a < b) (h : ∀ c, a ≤ c → c ≤ b → c = a ∨ c = b) : a ⋖ b
Full source 
theorem covBy_of_eq_or_eq (hab : a < b) (h : ∀ c, a ≤ c → c ≤ b → c = a ∨ c = b) : a ⋖ b :=
  ⟨hab, fun c ha hb => (h c ha.le hb.le).elim ha.ne' hb.ne⟩
Covering Relation from Maximal Intermediate Elements
Informal description
For elements $a$ and $b$ in a preorder, if $a < b$ and for every element $c$ satisfying $a \leq c \leq b$ we have $c = a$ or $c = b$, then $b$ covers $a$ (denoted $a \lessdot b$).
OrderEmbedding.covBy_of_apply theorem
{α β : Type*} [Preorder α] [Preorder β] (f : α ↪o β) {x y : α} (h : f x ⋖ f y) : x ⋖ y
Full source 
theorem OrderEmbedding.covBy_of_apply {α β : Type*} [Preorder α] [Preorder β]
    (f : α ↪o β) {x y : α} (h : f x ⋖ f y) : x ⋖ y := by
  use f.lt_iff_lt.1 h.1
  intro a
  rw [← f.lt_iff_lt, ← f.lt_iff_lt]
  apply h.2
Order Embedding Reflects Covering Relation
Informal description
Let $\alpha$ and $\beta$ be preordered types, and let $f \colon \alpha \hookrightarrow \beta$ be an order embedding. For any elements $x, y \in \alpha$, if $f(x) \lessdot f(y)$ in $\beta$, then $x \lessdot y$ in $\alpha$.
OrderIso.map_covBy theorem
{α β : Type*} [Preorder α] [Preorder β] (f : α ≃o β) {x y : α} : f x ⋖ f y ↔ x ⋖ y
Full source 
theorem OrderIso.map_covBy {α β : Type*} [Preorder α] [Preorder β]
    (f : α ≃o β) {x y : α} : f x ⋖ f yf x ⋖ f y ↔ x ⋖ y := by
  use f.toOrderEmbedding.covBy_of_apply
  conv_lhs => rw [← f.symm_apply_apply x, ← f.symm_apply_apply y]
  exact f.symm.toOrderEmbedding.covBy_of_apply
Order Isomorphism Preserves Covering Relation: $f(x) \lessdot f(y) \leftrightarrow x \lessdot y$
Informal description
Let $\alpha$ and $\beta$ be preordered types, and let $f \colon \alpha \simeq_o \beta$ be an order isomorphism. For any elements $x, y \in \alpha$, the image $f(y)$ covers $f(x)$ in $\beta$ if and only if $y$ covers $x$ in $\alpha$, i.e., $f(x) \lessdot f(y) \leftrightarrow x \lessdot y$.
WCovBy.covBy_of_ne theorem
(h : a ⩿ b) (h2 : a ≠ b) : a ⋖ b
Full source 
theorem WCovBy.covBy_of_ne (h : a ⩿ b) (h2 : a ≠ b) : a ⋖ b :=
  ⟨h.le.lt_of_ne h2, h.2⟩
Weak Covering with Inequality Implies Covering
Informal description
If $b$ weakly covers $a$ (denoted $a \⩿ b$) and $a \neq b$, then $b$ covers $a$ (denoted $a \⋖ b$).
covBy_iff_lt_and_eq_or_eq theorem
: a ⋖ b ↔ a < b ∧ ∀ c, a ≤ c → c ≤ b → c = a ∨ c = b
Full source 
/-- An `iff` version of `CovBy.eq_or_eq` and `covBy_of_eq_or_eq`. -/
theorem covBy_iff_lt_and_eq_or_eq : a ⋖ ba ⋖ b ↔ a < b ∧ ∀ c, a ≤ c → c ≤ b → c = a ∨ c = b :=
  ⟨fun h => ⟨h.lt, fun _ => h.eq_or_eq⟩, And.rec covBy_of_eq_or_eq⟩
Characterization of Covering Relation via Maximal Intermediate Elements
Informal description
For elements $a$ and $b$ in a preorder, $b$ covers $a$ (denoted $a \lessdot b$) if and only if $a < b$ and for every element $c$ satisfying $a \leq c \leq b$, we have $c = a$ or $c = b$.
CovBy.Ico_eq theorem
(h : a ⋖ b) : Ico a b = { a }
Full source 
theorem CovBy.Ico_eq (h : a ⋖ b) : Ico a b = {a} := by
  rw [← Ioo_union_left h.lt, h.Ioo_eq, empty_union]
Covering Relation Yields Singleton Left-Closed Interval: $a \lessdot b \Rightarrow [a, b) = \{a\}$
Informal description
If $b$ covers $a$ (denoted $a \lessdot b$) in a preorder, then the left-closed right-open interval $[a, b)$ is equal to the singleton set $\{a\}$.
CovBy.Ioc_eq theorem
(h : a ⋖ b) : Ioc a b = { b }
Full source 
theorem CovBy.Ioc_eq (h : a ⋖ b) : Ioc a b = {b} := by
  rw [← Ioo_union_right h.lt, h.Ioo_eq, empty_union]
Covering Relation Yields Singleton Right-Closed Interval: $a \lessdot b \Rightarrow (a, b] = \{b\}$
Informal description
If $b$ covers $a$ (denoted $a \lessdot b$) in a preorder, then the left-open right-closed interval $(a, b]$ is equal to the singleton set $\{b\}$, i.e., $\text{Ioc}(a, b) = \{b\}$.
CovBy.Icc_eq theorem
(h : a ⋖ b) : Icc a b = { a, b }
Full source 
theorem CovBy.Icc_eq (h : a ⋖ b) : Icc a b = {a, b} :=
  h.wcovBy.Icc_eq
Covering Relation Yields Two-Element Closed Interval: $a \lessdot b \Rightarrow [a, b] = \{a, b\}$
Informal description
For any elements $a$ and $b$ in a preorder, if $b$ covers $a$ (denoted $a \lessdot b$), then the closed interval $[a, b]$ is equal to the two-element set $\{a, b\}$.
CovBy.Ioi_eq theorem
(h : a ⋖ b) : Ioi a = Ici b
Full source 
theorem CovBy.Ioi_eq (h : a ⋖ b) : Ioi a = Ici b := by
  rw [← Ioo_union_Ici_eq_Ioi h.lt, h.Ioo_eq, empty_union]
Covering Relation Equates Right-Infinite Intervals: $a \lessdot b \Rightarrow (a, \infty) = [b, \infty)$
Informal description
If $b$ covers $a$ (denoted $a \lessdot b$) in a preorder, then the open right-infinite interval $(a, \infty)$ is equal to the closed right-infinite interval $[b, \infty)$, i.e., $\text{Ioi}(a) = \text{Ici}(b)$.
CovBy.Iio_eq theorem
(h : a ⋖ b) : Iio b = Iic a
Full source 
theorem CovBy.Iio_eq (h : a ⋖ b) : Iio b = Iic a := by
  rw [← Iic_union_Ioo_eq_Iio h.lt, h.Ioo_eq, union_empty]
Covering Relation Implies $(-\infty, b) = (-\infty, a]$
Informal description
If $b$ covers $a$ (denoted $a \lessdot b$) in a preorder, then the left-infinite right-open interval $(-\infty, b)$ is equal to the left-infinite right-closed interval $(-\infty, a]$. In other words, $\{x \mid x < b\} = \{x \mid x \leq a\}$.
WCovBy.le_of_lt theorem
(hab : a ⩿ b) (hcb : c < b) : c ≤ a
Full source 
theorem WCovBy.le_of_lt (hab : a ⩿ b) (hcb : c < b) : c ≤ a :=
  not_lt.1 fun hac => hab.2 hac hcb
Weak Covering Implies Lower Bound: $a ⩿ b$ and $c < b$ implies $c \leq a$
Informal description
If $b$ weakly covers $a$ (denoted $a ⩿ b$) and $c < b$, then $c \leq a$.
WCovBy.ge_of_gt theorem
(hab : a ⩿ b) (hac : a < c) : b ≤ c
Full source 
theorem WCovBy.ge_of_gt (hab : a ⩿ b) (hac : a < c) : b ≤ c :=
  not_lt.1 <| hab.2 hac
Upper Bound Property for Weakly Covering Elements
Informal description
Let $a$ and $b$ be elements in a partially ordered set such that $b$ weakly covers $a$ (denoted $a ⩿ b$). If $a < c$ for some element $c$, then $b \leq c$.
CovBy.le_of_lt theorem
(hab : a ⋖ b) : c < b → c ≤ a
Full source 
theorem CovBy.le_of_lt (hab : a ⋖ b) : c < b → c ≤ a :=
  hab.wcovBy.le_of_lt
Covering Implies Lower Bound: $a \lessdot b$ and $c < b$ implies $c \leq a$
Informal description
If $b$ covers $a$ (denoted $a \lessdot b$) and $c < b$, then $c \leq a$.
CovBy.ge_of_gt theorem
(hab : a ⋖ b) : a < c → b ≤ c
Full source 
theorem CovBy.ge_of_gt (hab : a ⋖ b) : a < c → b ≤ c :=
  hab.wcovBy.ge_of_gt
Covering Implies Upper Bound: $a \lessdot b$ and $a < c$ implies $b \leq c$
Informal description
If $b$ covers $a$ (denoted $a \lessdot b$) and $a < c$ for some element $c$, then $b \leq c$.
CovBy.unique_left theorem
(ha : a ⋖ c) (hb : b ⋖ c) : a = b
Full source 
theorem CovBy.unique_left (ha : a ⋖ c) (hb : b ⋖ c) : a = b :=
  (hb.le_of_lt ha.lt).antisymm <| ha.le_of_lt hb.lt
Uniqueness of Left Cover in a Covering Relation
Informal description
If two elements $a$ and $b$ both cover the same element $c$ (i.e., $a \lessdot c$ and $b \lessdot c$), then $a = b$.
CovBy.unique_right theorem
(hb : a ⋖ b) (hc : a ⋖ c) : b = c
Full source 
theorem CovBy.unique_right (hb : a ⋖ b) (hc : a ⋖ c) : b = c :=
  (hb.ge_of_gt hc.lt).antisymm <| hc.ge_of_gt hb.lt
Right-Uniqueness of the Covering Relation: $a \lessdot b$ and $a \lessdot c$ implies $b = c$
Informal description
If $b$ covers $a$ (denoted $a \lessdot b$) and $c$ also covers $a$ (denoted $a \lessdot c$), then $b = c$. In other words, the covering relation is right-unique: an element cannot be covered by two distinct elements.
covBy_iff_lt_iff_le_left theorem
{x y : α} : x ⋖ y ↔ ∀ {z}, z < y ↔ z ≤ x
Full source 
theorem covBy_iff_lt_iff_le_left {x y : α} : x ⋖ yx ⋖ y ↔ ∀ {z}, z < y ↔ z ≤ x where
  mp := fun hx _z ↦ ⟨hx.le_of_lt, fun hz ↦ hz.trans_lt hx.lt⟩
  mpr := fun H ↦ ⟨H.2 le_rfl, fun _z hx hz ↦ (H.1 hz).not_lt hx⟩
Covering Relation Characterization via Left Comparison: $x \lessdot y \leftrightarrow (\forall z, z < y \leftrightarrow z \leq x)$
Informal description
For any elements $x$ and $y$ in a linearly ordered set $\alpha$, the relation $y$ covers $x$ (denoted $x \lessdot y$) holds if and only if for every element $z \in \alpha$, the inequality $z < y$ is equivalent to $z \leq x$.
covBy_iff_le_iff_lt_left theorem
{x y : α} : x ⋖ y ↔ ∀ {z}, z ≤ x ↔ z < y
Full source 
theorem covBy_iff_le_iff_lt_left {x y : α} : x ⋖ yx ⋖ y ↔ ∀ {z}, z ≤ x ↔ z < y := by
  simp_rw [covBy_iff_lt_iff_le_left, iff_comm]
Covering relation characterization via inequalities
Informal description
Let $\alpha$ be a linearly ordered set. For elements $x, y \in \alpha$, $y$ covers $x$ (denoted $x \lessdot y$) if and only if for every element $z \in \alpha$, $z \leq x$ is equivalent to $z < y$.
covBy_iff_lt_iff_le_right theorem
{x y : α} : x ⋖ y ↔ ∀ {z}, x < z ↔ y ≤ z
Full source 
theorem covBy_iff_lt_iff_le_right {x y : α} : x ⋖ yx ⋖ y ↔ ∀ {z}, x < z ↔ y ≤ z := by
  trans ∀ {z}, ¬ z ≤ x¬ z ≤ x ↔ ¬ z < y
  · simp_rw [covBy_iff_le_iff_lt_left, not_iff_not]
  · simp
Covering Relation Characterization via Right Comparison
Informal description
For elements $x$ and $y$ in a partially ordered set, $y$ covers $x$ (denoted $x \lessdot y$) if and only if for every element $z$, the relation $x < z$ is equivalent to $y \leq z$.
covBy_iff_le_iff_lt_right theorem
{x y : α} : x ⋖ y ↔ ∀ {z}, y ≤ z ↔ x < z
Full source 
theorem covBy_iff_le_iff_lt_right {x y : α} : x ⋖ yx ⋖ y ↔ ∀ {z}, y ≤ z ↔ x < z := by
  simp_rw [covBy_iff_lt_iff_le_right, iff_comm]
Covering Relation Characterization via Right Inequalities
Informal description
For elements $x$ and $y$ in a linearly ordered set $\alpha$, $y$ covers $x$ (denoted $x \lessdot y$) if and only if for every element $z$, the inequality $y \leq z$ holds precisely when $x < z$.
LT.lt.exists_disjoint_Iio_Ioi theorem
(h : a < b) : ∃ a' > a, ∃ b' < b, ∀ x < a', ∀ y > b', x < y
Full source 
/-- 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'`. -/
lemma LT.lt.exists_disjoint_Iio_Ioi (h : a < b) :
    ∃ a' > a, ∃ b' < b, ∀ x < a', ∀ y > b', x < y := by
  by_cases h' : a ⋖ b
  · exact ⟨b, h, a, h, fun x hx y hy => hx.trans_le <| h'.ge_of_gt hy⟩
  · rcases h.exists_lt_lt h' with ⟨c, ha, hb⟩
    exact ⟨c, ha, c, hb, fun _ h₁ _ => lt_trans h₁⟩
Existence of Disjoint Intervals Around Strictly Ordered Elements in a Linear Order
Informal description
For any elements $a$ and $b$ in a linear order with $a < b$, there exist elements $a' > a$ and $b' < b$ such that for all $x < a'$ and $y > b'$, we have $x < y$. In other words, the interval $(-\infty, a')$ is strictly to the left of the interval $(b', \infty)$.
Bool.wcovBy_iff theorem
: ∀ {a b : Bool}, a ⩿ b ↔ a ≤ b
Full source 
@[simp] theorem wcovBy_iff : ∀ {a b : Bool}, a ⩿ ba ⩿ b ↔ a ≤ b := by unfold WCovBy; decide
Weak Covering Relation in Booleans: $a \lessapprox b \leftrightarrow a \leq b$
Informal description
For any two boolean values $a$ and $b$, $b$ weakly covers $a$ (denoted $a \lessapprox b$) if and only if $a$ is less than or equal to $b$ (denoted $a \leq b$).
Bool.covBy_iff theorem
: ∀ {a b : Bool}, a ⋖ b ↔ a < b
Full source 
@[simp] theorem covBy_iff : ∀ {a b : Bool}, a ⋖ ba ⋖ b ↔ a < b := by unfold CovBy; decide
Covering relation in booleans: $a \lessdot b \leftrightarrow a < b$
Informal description
For any two boolean values $a$ and $b$, $b$ covers $a$ (denoted $a \lessdot b$) if and only if $a$ is strictly less than $b$ (denoted $a < b$).
Bool.instDecidableRelWCovBy instance
: DecidableRel (· ⩿ · : Bool → Bool → Prop)
Full source 
instance instDecidableRelWCovBy : DecidableRel (· ⩿ · : Bool → Bool → Prop) := fun _ _ ↦
  decidable_of_iff _ wcovBy_iff.symm
Decidability of the Weak Covering Relation on Booleans
Informal description
For any two boolean values $a$ and $b$, the weak covering relation $a \lessapprox b$ is decidable.
Bool.instDecidableRelCovBy instance
: DecidableRel (· ⋖ · : Bool → Bool → Prop)
Full source 
instance instDecidableRelCovBy : DecidableRel (· ⋖ · : Bool → Bool → Prop) := fun _ _ ↦
  decidable_of_iff _ covBy_iff.symm
Decidability of the Covering Relation on Booleans
Informal description
For any two boolean values $a$ and $b$, the covering relation $a \lessdot b$ is decidable.
Set.wcovBy_insert theorem
(x : α) (s : Set α) : s ⩿ insert x s
Full source 
@[simp] lemma wcovBy_insert (x : α) (s : Set α) : s ⩿ insert x s := by
  refine wcovBy_of_eq_or_eq (subset_insert x s) fun t hst h2t => ?_
  by_cases h : x ∈ t
  · exact Or.inr (subset_antisymm h2t <| insert_subset_iff.mpr ⟨h, hst⟩)
  · refine Or.inl (subset_antisymm ?_ hst)
    rwa [← diff_singleton_eq_self h, diff_singleton_subset_iff]
Weak Covering Property of Set Insertion: $s \lessapprox \{x\} \cup s$
Informal description
For any element $x$ of type $\alpha$ and any set $s$ of elements of type $\alpha$, the set $\{x\} \cup s$ weakly covers $s$ (denoted $s \lessapprox \{x\} \cup s$). This means that $s \subseteq \{x\} \cup s$ and there is no set strictly between $s$ and $\{x\} \cup s$ in the subset order.
Set.sdiff_singleton_wcovBy theorem
(s : Set α) (a : α) : s \ { a } ⩿ s
Full source 
@[simp] lemma sdiff_singleton_wcovBy (s : Set α) (a : α) : s \ {a}s \ {a} ⩿ s := by
  by_cases ha : a ∈ s
  · convert wcovBy_insert a _
    ext
    simp [ha]
  · simp [ha]
Weak Covering Property of Set Difference with Singleton: $s \setminus \{a\} \lessapprox s$
Informal description
For any set $s$ over a type $\alpha$ and any element $a \in \alpha$, the set difference $s \setminus \{a\}$ weakly covers $s$ (denoted $s \setminus \{a\} \lessapprox s$). This means that $s \setminus \{a\} \subseteq s$ and there is no set strictly between $s \setminus \{a\}$ and $s$ in the subset order.
Set.covBy_insert theorem
(ha : a ∉ s) : s ⋖ insert a s
Full source 
@[simp] lemma covBy_insert (ha : a ∉ s) : s ⋖ insert a s :=
  (wcovBy_insert _ _).covBy_of_lt <| ssubset_insert ha
Covering Property of Set Insertion: $s \lessdot \{a\} \cup s$ for $a \notin s$
Informal description
For any set $s$ of elements of type $\alpha$ and any element $a \notin s$, the set $\{a\} \cup s$ covers $s$ (denoted $s \lessdot \{a\} \cup s$). This means that $s$ is strictly included in $\{a\} \cup s$ and there is no set strictly between $s$ and $\{a\} \cup s$ in the subset order.
Set.sdiff_singleton_covBy theorem
(ha : a ∈ s) : s \ { a } ⋖ s
Full source 
@[simp] lemma sdiff_singleton_covBy (ha : a ∈ s) : s \ {a}s \ {a} ⋖ s :=
  ⟨sdiff_lt (singleton_subset_iff.2 ha) <| singleton_ne_empty _, (sdiff_singleton_wcovBy _ _).2⟩
Covering Property of Set Difference with Singleton: $s \setminus \{a\} \lessdot s$ for $a \in s$
Informal description
For any set $s$ over a type $\alpha$ and any element $a \in s$, the set difference $s \setminus \{a\}$ covers $s$ (denoted $s \setminus \{a\} \lessdot s$). This means that $s \setminus \{a\}$ is strictly included in $s$ and there is no set strictly between $s \setminus \{a\}$ and $s$ in the subset order.
CovBy.exists_set_insert theorem
(h : s ⋖ t) : ∃ a ∉ s, insert a s = t
Full source 
lemma _root_.CovBy.exists_set_insert (h : s ⋖ t) : ∃ a ∉ s, insert a s = t :=
  let ⟨a, ha, hst⟩ := ssubset_iff_insert.1 h.lt
  ⟨a, ha, (hst.eq_of_not_ssuperset <| h.2 <| ssubset_insert ha).symm⟩
Existence of Inserted Element in Covering Relation for Sets
Informal description
If a set $t$ covers a set $s$ (denoted $s \lessdot t$), then there exists an element $a \notin s$ such that $t$ is equal to the set obtained by inserting $a$ into $s$, i.e., $t = \{a\} \cup s$.
CovBy.exists_set_sdiff_singleton theorem
(h : s ⋖ t) : ∃ a ∈ t, t \ { a } = s
Full source 
lemma _root_.CovBy.exists_set_sdiff_singleton (h : s ⋖ t) : ∃ a ∈ t, t \ {a} =  s :=
  let ⟨a, ha, hst⟩ := ssubset_iff_sdiff_singleton.1 h.lt
  ⟨a, ha, (hst.eq_of_not_ssubset fun h' ↦ h.2 h' <|
    sdiff_lt (singleton_subset_iff.2 ha) <| singleton_ne_empty _).symm⟩
Existence of Removed Element in Covering Relation for Sets: $s \lessdot t \implies \exists a \in t, t \setminus \{a\} = s$
Informal description
If a set $t$ covers a set $s$ (denoted $s \lessdot t$), then there exists an element $a \in t$ such that $t \setminus \{a\} = s$.
Set.covBy_iff_exists_insert theorem
: s ⋖ t ↔ ∃ a ∉ s, insert a s = t
Full source 
lemma covBy_iff_exists_insert : s ⋖ ts ⋖ t ↔ ∃ a ∉ s, insert a s = t :=
  ⟨CovBy.exists_set_insert, by rintro ⟨a, ha, rfl⟩; exact covBy_insert ha⟩
Characterization of Set Covering via Insertion: $s \lessdot t \iff \exists a \notin s, t = \{a\} \cup s$
Informal description
For any two sets $s$ and $t$ of elements of type $\alpha$, the set $t$ covers $s$ (denoted $s \lessdot t$) if and only if there exists an element $a \notin s$ such that $t = \{a\} \cup s$.
Set.covBy_iff_exists_sdiff_singleton theorem
: s ⋖ t ↔ ∃ a ∈ t, t \ { a } = s
Full source 
lemma covBy_iff_exists_sdiff_singleton : s ⋖ ts ⋖ t ↔ ∃ a ∈ t, t \ {a} = s :=
  ⟨CovBy.exists_set_sdiff_singleton, by rintro ⟨a, ha, rfl⟩; exact sdiff_singleton_covBy ha⟩
Characterization of Set Covering via Singleton Removal: $s \lessdot t \iff \exists a \in t, t \setminus \{a\} = s$
Informal description
For any two sets $s$ and $t$ of elements of type $\alpha$, the set $t$ covers $s$ (denoted $s \lessdot t$) if and only if there exists an element $a \in t$ such that $t \setminus \{a\} = s$.
wcovBy_eq_reflGen_covBy theorem
[PartialOrder α] : ((· : α) ⩿ ·) = ReflGen (· ⋖ ·)
Full source 
lemma wcovBy_eq_reflGen_covBy [PartialOrder α] : ((· : α) ⩿ ·) = ReflGen (· ⋖ ·) := by
  ext x y; simp_rw [wcovBy_iff_eq_or_covBy, @eq_comm _ x, reflGen_iff]
Weakly Covers Equals Reflexive Closure of Covers in Partial Orders
Informal description
In a partial order $\alpha$, the weakly covers relation $a \lessdot b$ (denoted by $a ⩿ b$) is equal to the reflexive closure of the covers relation $a ⋖ b$. That is, $a ⩿ b$ holds if and only if either $a ⋖ b$ or $a = b$.
transGen_wcovBy_eq_reflTransGen_covBy theorem
[PartialOrder α] : TransGen ((· : α) ⩿ ·) = ReflTransGen (· ⋖ ·)
Full source 
lemma transGen_wcovBy_eq_reflTransGen_covBy [PartialOrder α] :
    TransGen ((· : α) ⩿ ·) = ReflTransGen (· ⋖ ·) := by
  rw [wcovBy_eq_reflGen_covBy, transGen_reflGen]
Transitive Closure of Weakly Covers Equals Reflexive Transitive Closure of Covers in Partial Orders
Informal description
In a partial order $\alpha$, the transitive closure of the weakly covers relation $a \lessdot b$ (denoted by $a ⩿ b$) is equal to the reflexive transitive closure of the covers relation $a ⋖ b$. That is, $\text{TransGen}(⩿) = \text{ReflTransGen}(⋖)$.
reflTransGen_wcovBy_eq_reflTransGen_covBy theorem
[PartialOrder α] : ReflTransGen ((· : α) ⩿ ·) = ReflTransGen (· ⋖ ·)
Full source 
lemma reflTransGen_wcovBy_eq_reflTransGen_covBy [PartialOrder α] :
    ReflTransGen ((· : α) ⩿ ·) = ReflTransGen (· ⋖ ·) := by
  rw [wcovBy_eq_reflGen_covBy, reflTransGen_reflGen]
Reflexive Transitive Closure of Weakly Covers Equals Reflexive Transitive Closure of Covers in Partial Orders
Informal description
In a partial order $\alpha$, the reflexive transitive closure of the weakly covers relation $a \lessdot b$ (denoted by $a ⩿ b$) is equal to the reflexive transitive closure of the covers relation $a ⋖ b$. That is, $\text{ReflTransGen}(⩿) = \text{ReflTransGen}(⋖)$.
Prod.swap_wcovBy_swap theorem
: x.swap ⩿ y.swap ↔ x ⩿ y
Full source 
@[simp]
theorem swap_wcovBy_swap : x.swap ⩿ y.swapx.swap ⩿ y.swap ↔ x ⩿ y :=
  apply_wcovBy_apply_iff (OrderIso.prodComm : α × βα × β ≃o β × α)
Weak Covering Relation is Preserved Under Product Swap: $y.swap ⩿ x.swap \leftrightarrow y ⩿ x$
Informal description
For any elements $x$ and $y$ in the product of two preordered types $\alpha \times \beta$, the swapped pair $y.swap$ weakly covers $x.swap$ (denoted $y.swap ⩿ x.swap$) if and only if $y$ weakly covers $x$ (denoted $y ⩿ x$).
Prod.swap_covBy_swap theorem
: x.swap ⋖ y.swap ↔ x ⋖ y
Full source 
@[simp]
theorem swap_covBy_swap : x.swap ⋖ y.swapx.swap ⋖ y.swap ↔ x ⋖ y :=
  apply_covBy_apply_iff (OrderIso.prodComm : α × βα × β ≃o β × α)
Covering Relation is Preserved Under Product Swap: $y.\text{swap} \lessdot x.\text{swap} \leftrightarrow y \lessdot x$
Informal description
For any elements $x$ and $y$ in the product of two preordered types $\alpha \times \beta$, the swapped pair $y.\text{swap}$ covers $x.\text{swap}$ (denoted $y.\text{swap} \lessdot x.\text{swap}$) if and only if $y$ covers $x$ (denoted $y \lessdot x$).
Prod.fst_eq_or_snd_eq_of_wcovBy theorem
: x ⩿ y → x.1 = y.1 ∨ x.2 = y.2
Full source 
theorem fst_eq_or_snd_eq_of_wcovBy : x ⩿ y → x.1 = y.1 ∨ x.2 = y.2 := by
  refine fun h => of_not_not fun hab => ?_
  push_neg at hab
  exact
    h.2 (mk_lt_mk.2 <| Or.inl ⟨hab.1.lt_of_le h.1.1, le_rfl⟩)
      (mk_lt_mk.2 <| Or.inr ⟨le_rfl, hab.2.lt_of_le h.1.2⟩)
Weak Covering in Product Order Implies Component Equality
Informal description
For any elements $x$ and $y$ in the product of two preordered types $\alpha \times \beta$, if $y$ weakly covers $x$ (denoted $x ⩿ y$), then either the first components are equal ($x_1 = y_1$) or the second components are equal ($x_2 = y_2$).
WCovBy.fst theorem
(h : x ⩿ y) : x.1 ⩿ y.1
Full source 
theorem _root_.WCovBy.fst (h : x ⩿ y) : x.1 ⩿ y.1 :=
  ⟨h.1.1, fun _ h₁ h₂ => h.2 (mk_lt_mk_iff_left.2 h₁) ⟨⟨h₂.le, h.1.2⟩, fun hc => h₂.not_le hc.1⟩⟩
Weak Covering Relation Preserved Under First Projection
Informal description
For any elements $x$ and $y$ in the product of two preordered types $\alpha \times \beta$, if $y$ weakly covers $x$ (denoted $x ⩿ y$), then the first component of $y$ weakly covers the first component of $x$ (i.e., $x.1 ⩿ y.1$).
WCovBy.snd theorem
(h : x ⩿ y) : x.2 ⩿ y.2
Full source 
theorem _root_.WCovBy.snd (h : x ⩿ y) : x.2 ⩿ y.2 :=
  ⟨h.1.2, fun _ h₁ h₂ => h.2 (mk_lt_mk_iff_right.2 h₁) ⟨⟨h.1.1, h₂.le⟩, fun hc => h₂.not_le hc.2⟩⟩
Weak Covering Relation Preserved Under Second Projection
Informal description
For any elements $x$ and $y$ in the product of two preordered types $\alpha \times \beta$, if $y$ weakly covers $x$ (denoted $x ⩿ y$), then the second component of $y$ weakly covers the second component of $x$ (i.e., $x.2 ⩿ y.2$).
Prod.mk_wcovBy_mk_iff_left theorem
: (a₁, b) ⩿ (a₂, b) ↔ a₁ ⩿ a₂
Full source 
theorem mk_wcovBy_mk_iff_left : (a₁, b)(a₁, b) ⩿ (a₂, b)(a₁, b) ⩿ (a₂, b) ↔ a₁ ⩿ a₂ := by
  refine ⟨WCovBy.fst, (And.imp mk_le_mk_iff_left.2) fun h c h₁ h₂ => ?_⟩
  have : c.2 = b := h₂.le.2.antisymm h₁.le.2
  rw [← @Prod.mk.eta _ _ c, this, mk_lt_mk_iff_left] at h₁ h₂
  exact h h₁ h₂
Weak Covering Relation in Product Preorder: Left Component Condition
Informal description
For any elements $a₁, a₂$ in a preordered type $\alpha$ and any element $b$ in a type $\beta$, the pair $(a₁, b)$ is weakly covered by $(a₂, b)$ (denoted $(a₁, b) ⩿ (a₂, b)$) if and only if $a₁$ is weakly covered by $a₂$ (denoted $a₁ ⩿ a₂$).
Prod.mk_wcovBy_mk_iff_right theorem
: (a, b₁) ⩿ (a, b₂) ↔ b₁ ⩿ b₂
Full source 
theorem mk_wcovBy_mk_iff_right : (a, b₁)(a, b₁) ⩿ (a, b₂)(a, b₁) ⩿ (a, b₂) ↔ b₁ ⩿ b₂ :=
  swap_wcovBy_swap.trans mk_wcovBy_mk_iff_left
Weak Covering Relation in Product Preorder: Right Component Condition
Informal description
For any elements $a$ in a preordered type $\alpha$ and any elements $b₁, b₂$ in a preordered type $\beta$, the pair $(a, b₁)$ is weakly covered by $(a, b₂)$ (denoted $(a, b₁) ⩿ (a, b₂)$) if and only if $b₁$ is weakly covered by $b₂$ (denoted $b₁ ⩿ b₂$).
Prod.mk_covBy_mk_iff_left theorem
: (a₁, b) ⋖ (a₂, b) ↔ a₁ ⋖ a₂
Full source 
theorem mk_covBy_mk_iff_left : (a₁, b)(a₁, b) ⋖ (a₂, b)(a₁, b) ⋖ (a₂, b) ↔ a₁ ⋖ a₂ := by
  simp_rw [covBy_iff_wcovBy_and_lt, mk_wcovBy_mk_iff_left, mk_lt_mk_iff_left]
Covering Relation in Product Preorder: Left Component Condition
Informal description
For any elements $a₁$, $a₂$, and $b$ in a preorder, the pair $(a₁, b)$ is covered by $(a₂, b)$ (denoted $(a₁, b) ⋖ (a₂, b)$) if and only if $a₁$ is covered by $a₂$ (denoted $a₁ ⋖ a₂$).
Prod.mk_covBy_mk_iff_right theorem
: (a, b₁) ⋖ (a, b₂) ↔ b₁ ⋖ b₂
Full source 
theorem mk_covBy_mk_iff_right : (a, b₁)(a, b₁) ⋖ (a, b₂)(a, b₁) ⋖ (a, b₂) ↔ b₁ ⋖ b₂ := by
  simp_rw [covBy_iff_wcovBy_and_lt, mk_wcovBy_mk_iff_right, mk_lt_mk_iff_right]
Covering Relation in Product Preorder: Right Component Condition
Informal description
For any elements $a$, $b₁$, and $b₂$ in a preorder, the pair $(a, b₁)$ is covered by $(a, b₂)$ (denoted $(a, b₁) ⋖ (a, b₂)$) if and only if $b₁$ is covered by $b₂$ (denoted $b₁ ⋖ b₂$).
Prod.mk_wcovBy_mk_iff theorem
: (a₁, b₁) ⩿ (a₂, b₂) ↔ a₁ ⩿ a₂ ∧ b₁ = b₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₂
Full source 
theorem mk_wcovBy_mk_iff : (a₁, b₁)(a₁, b₁) ⩿ (a₂, b₂)(a₁, b₁) ⩿ (a₂, b₂) ↔ a₁ ⩿ a₂ ∧ b₁ = b₂ ∨ b₁ ⩿ b₂ ∧ a₁ = a₂ := by
  refine ⟨fun h => ?_, ?_⟩
  · obtain rfl | rfl : a₁ = a₂ ∨ b₁ = b₂ := fst_eq_or_snd_eq_of_wcovBy h
    · exact Or.inr ⟨mk_wcovBy_mk_iff_right.1 h, rfl⟩
    · exact Or.inl ⟨mk_wcovBy_mk_iff_left.1 h, rfl⟩
  · rintro (⟨h, rfl⟩ | ⟨h, rfl⟩)
    · exact mk_wcovBy_mk_iff_left.2 h
    · exact mk_wcovBy_mk_iff_right.2 h
Weak Covering Relation in Product Preorder: Component-wise Characterization
Informal description
For elements $(a₁, b₁)$ and $(a₂, b₂)$ in the product of two preordered types $\alpha \times \beta$, the pair $(a₂, b₂)$ weakly covers $(a₁, b₁)$ (denoted $(a₁, b₁) ⩿ (a₂, b₂)$) if and only if either: 1. $a₂$ weakly covers $a₁$ (denoted $a₁ ⩿ a₂$) and $b₁ = b₂$, or 2. $b₂$ weakly covers $b₁$ (denoted $b₁ ⩿ b₂$) and $a₁ = a₂$.
Prod.mk_covBy_mk_iff theorem
: (a₁, b₁) ⋖ (a₂, b₂) ↔ a₁ ⋖ a₂ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₂
Full source 
theorem mk_covBy_mk_iff : (a₁, b₁)(a₁, b₁) ⋖ (a₂, b₂)(a₁, b₁) ⋖ (a₂, b₂) ↔ a₁ ⋖ a₂ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₂ := by
  refine ⟨fun h => ?_, ?_⟩
  · obtain rfl | rfl : a₁ = a₂ ∨ b₁ = b₂ := fst_eq_or_snd_eq_of_wcovBy h.wcovBy
    · exact Or.inr ⟨mk_covBy_mk_iff_right.1 h, rfl⟩
    · exact Or.inl ⟨mk_covBy_mk_iff_left.1 h, rfl⟩
  · rintro (⟨h, rfl⟩ | ⟨h, rfl⟩)
    · exact mk_covBy_mk_iff_left.2 h
    · exact mk_covBy_mk_iff_right.2 h
Covering Relation in Product Preorder: Component-wise Characterization
Informal description
For elements $(a₁, b₁)$ and $(a₂, b₂)$ in the product of two preordered types $\alpha \times \beta$, the pair $(a₂, b₂)$ covers $(a₁, b₁)$ (denoted $(a₁, b₁) \lessdot (a₂, b₂)$) if and only if either: 1. $a₂$ covers $a₁$ (denoted $a₁ \lessdot a₂$) and $b₁ = b₂$, or 2. $b₂$ covers $b₁$ (denoted $b₁ \lessdot b₂$) and $a₁ = a₂$.
Prod.wcovBy_iff theorem
: x ⩿ y ↔ x.1 ⩿ y.1 ∧ x.2 = y.2 ∨ x.2 ⩿ y.2 ∧ x.1 = y.1
Full source 
theorem wcovBy_iff : x ⩿ yx ⩿ y ↔ x.1 ⩿ y.1 ∧ x.2 = y.2 ∨ x.2 ⩿ y.2 ∧ x.1 = y.1 := by
  cases x
  cases y
  exact mk_wcovBy_mk_iff
Weak Covering Relation in Product Preorder: Component-wise Characterization
Informal description
For elements $x = (x_1, x_2)$ and $y = (y_1, y_2)$ in the product of two preordered types $\alpha \times \beta$, the element $y$ weakly covers $x$ (denoted $x \⩿ y$) if and only if either: 1. $y_1$ weakly covers $x_1$ (denoted $x_1 \⩿ y_1$) and $x_2 = y_2$, or 2. $y_2$ weakly covers $x_2$ (denoted $x_2 \⩿ y_2$) and $x_1 = y_1$.
Prod.covBy_iff theorem
: x ⋖ y ↔ x.1 ⋖ y.1 ∧ x.2 = y.2 ∨ x.2 ⋖ y.2 ∧ x.1 = y.1
Full source 
theorem covBy_iff : x ⋖ yx ⋖ y ↔ x.1 ⋖ y.1 ∧ x.2 = y.2 ∨ x.2 ⋖ y.2 ∧ x.1 = y.1 := by
  cases x
  cases y
  exact mk_covBy_mk_iff
Covering Relation in Product Preorder: Component-wise Characterization
Informal description
For elements $x = (x_1, x_2)$ and $y = (y_1, y_2)$ in the product of two preordered types $\alpha \times \beta$, the element $y$ covers $x$ (denoted $x \lessdot y$) if and only if either: 1. $y_1$ covers $x_1$ (denoted $x_1 \lessdot y_1$) and $x_2 = y_2$, or 2. $y_2$ covers $x_2$ (denoted $x_2 \lessdot y_2$) and $x_1 = y_1$.
WithTop.coe_wcovBy_coe theorem
: (a : WithTop α) ⩿ b ↔ a ⩿ b
Full source 
@[simp, norm_cast] lemma coe_wcovBy_coe : (a : WithTop α) ⩿ b(a : WithTop α) ⩿ b ↔ a ⩿ b :=
  Set.OrdConnected.apply_wcovBy_apply_iff OrderEmbedding.withTopCoe <| by
    simp [WithTop.range_coe, ordConnected_Iio]
Weak Covering Relation Preserved in Extended Type: $a \⩿ b \leftrightarrow a \⩿ b$ in $\text{WithTop} \alpha$
Informal description
For any elements $a, b$ in the type $\alpha$ extended with a top element $\top$, the weakly covering relation $a \⩿ b$ holds in $\text{WithTop} \alpha$ if and only if it holds in $\alpha$.
WithTop.coe_covBy_coe theorem
: (a : WithTop α) ⋖ b ↔ a ⋖ b
Full source 
@[simp, norm_cast] lemma coe_covBy_coe : (a : WithTop α) ⋖ b(a : WithTop α) ⋖ b ↔ a ⋖ b :=
  Set.OrdConnected.apply_covBy_apply_iff OrderEmbedding.withTopCoe <| by
    simp [WithTop.range_coe, ordConnected_Iio]
Covering Relation Preserved in Extended Type: $a \lessdot b \leftrightarrow a \lessdot b$ in $\text{WithTop} \alpha$
Informal description
For any elements $a, b$ in the type $\alpha$ extended with a top element $\top$, the covering relation $a \lessdot b$ holds in $\text{WithTop} \alpha$ if and only if it holds in $\alpha$.
WithTop.coe_covBy_top theorem
: (a : WithTop α) ⋖ ⊤ ↔ IsMax a
Full source 
@[simp] lemma coe_covBy_top : (a : WithTop α) ⋖ ⊤(a : WithTop α) ⋖ ⊤ ↔ IsMax a := by
  simp only [covBy_iff_Ioo_eq, ← image_coe_Ioi, coe_lt_top, image_eq_empty,
    true_and, Ioi_eq_empty_iff]
Covering relation between an element and top in extended type: $a \lessdot \top \leftrightarrow \text{IsMax}(a)$
Informal description
For any element $a$ in the type $\alpha$ extended with a top element $\top$, the top element $\top$ covers $a$ (denoted $a \lessdot \top$) if and only if $a$ is a maximal element in $\alpha$.
WithTop.coe_wcovBy_top theorem
: (a : WithTop α) ⩿ ⊤ ↔ IsMax a
Full source 
@[simp] lemma coe_wcovBy_top : (a : WithTop α) ⩿ ⊤(a : WithTop α) ⩿ ⊤ ↔ IsMax a := by
  simp only [wcovBy_iff_Ioo_eq, ← image_coe_Ioi, le_top, image_eq_empty, true_and, Ioi_eq_empty_iff]
Weak Covering Relation Between Element and Top in Extended Type: $a \lessdot \top \leftrightarrow \text{IsMax}(a)$
Informal description
For any element $a$ in the type $\alpha$ extended with a top element $\top$, the top element $\top$ weakly covers $a$ (denoted $a \lessdot \top$) if and only if $a$ is a maximal element in $\alpha$.
WithBot.coe_wcovBy_coe theorem
: (a : WithBot α) ⩿ b ↔ a ⩿ b
Full source 
@[simp, norm_cast] lemma coe_wcovBy_coe : (a : WithBot α) ⩿ b(a : WithBot α) ⩿ b ↔ a ⩿ b :=
  Set.OrdConnected.apply_wcovBy_apply_iff OrderEmbedding.withBotCoe <| by
    simp [WithBot.range_coe, ordConnected_Ioi]
Weak Covering Relation Preservation Under Canonical Embedding into $\text{WithBot} \alpha$
Informal description
For any elements $a$ and $b$ in a preorder $\alpha$, the weakly covering relation $a \⩿ b$ holds in $\alpha$ if and only if the weakly covering relation $\text{some}(a) \⩿ \text{some}(b)$ holds in $\text{WithBot} \alpha$, where $\text{some} \colon \alpha \to \text{WithBot} \alpha$ is the canonical embedding.
WithBot.coe_covBy_coe theorem
: (a : WithBot α) ⋖ b ↔ a ⋖ b
Full source 
@[simp, norm_cast] lemma coe_covBy_coe : (a : WithBot α) ⋖ b(a : WithBot α) ⋖ b ↔ a ⋖ b :=
  Set.OrdConnected.apply_covBy_apply_iff OrderEmbedding.withBotCoe <| by
    simp [WithBot.range_coe, ordConnected_Ioi]
Covering Relation Preservation Under Canonical Embedding into $\operatorname{WithBot} \alpha$
Informal description
For any elements $a$ and $b$ in a preorder $\alpha$, the covering relation $a \lessdot b$ holds in $\alpha$ if and only if the covering relation $\operatorname{some}(a) \lessdot \operatorname{some}(b)$ holds in $\operatorname{WithBot} \alpha$, where $\operatorname{some} \colon \alpha \to \operatorname{WithBot} \alpha$ is the canonical embedding.
WithBot.bot_covBy_coe theorem
: ⊥ ⋖ (a : WithBot α) ↔ IsMin a
Full source 
@[simp] lemma bot_covBy_coe : ⊥⊥ ⋖ (a : WithBot α)⊥ ⋖ (a : WithBot α) ↔ IsMin a := by
  simp only [covBy_iff_Ioo_eq, ← image_coe_Iio, bot_lt_coe, image_eq_empty,
    true_and, Iio_eq_empty_iff]
Bottom Element Covers $a$ iff $a$ is Minimal in $\alpha$
Informal description
In a preorder $\alpha$, the bottom element $\bot$ in $\text{WithBot }\alpha$ covers an element $a$ (denoted $\bot \lessdot a$) if and only if $a$ is a minimal element in $\alpha$.
WithBot.bot_wcovBy_coe theorem
: ⊥ ⩿ (a : WithBot α) ↔ IsMin a
Full source 
@[simp] lemma bot_wcovBy_coe : ⊥⊥ ⩿ (a : WithBot α)⊥ ⩿ (a : WithBot α) ↔ IsMin a := by
  simp only [wcovBy_iff_Ioo_eq, ← image_coe_Iio, bot_le, image_eq_empty, true_and, Iio_eq_empty_iff]
Weak Covering by Bottom Element iff Minimal in $\alpha$
Informal description
For any element $a$ in a preorder $\alpha$, the bottom element $\bot$ in $\text{WithBot }\alpha$ weakly covers $a$ (denoted $\bot \lessdot a$) if and only if $a$ is a minimal element in $\alpha$.
exists_covBy_of_wellFoundedLT theorem
[wf : WellFoundedLT α] ⦃a : α⦄ (h : ¬IsMax a) : ∃ a', a ⋖ a'
Full source 
lemma exists_covBy_of_wellFoundedLT [wf : WellFoundedLT α] ⦃a : α⦄ (h : ¬ IsMax a) :
    ∃ a', a ⋖ a' := by
  rw [not_isMax_iff] at h
  exact ⟨_, wellFounded_lt.min_mem _ h, fun a' ↦ wf.wf.not_lt_min _ h⟩
Existence of Covering Element in Well-Founded Orders for Non-Maximal Elements
Informal description
Let $\alpha$ be a type with a well-founded strict less-than relation $<$. For any element $a \in \alpha$ that is not maximal, there exists an element $a' \in \alpha$ such that $a'$ covers $a$ (i.e., $a \lessdot a'$).
exists_covBy_of_wellFoundedGT theorem
[wf : WellFoundedGT α] ⦃a : α⦄ (h : ¬IsMin a) : ∃ a', a' ⋖ a
Full source 
lemma exists_covBy_of_wellFoundedGT [wf : WellFoundedGT α] ⦃a : α⦄ (h : ¬ IsMin a) :
    ∃ a', a' ⋖ a := by
  rw [not_isMin_iff] at h
  exact ⟨_, wf.wf.min_mem _ h, fun a' h₁ h₂ ↦ wf.wf.not_lt_min _ h h₂ h₁⟩
Existence of Covering Element for Non-Minimal Elements in Well-Founded GT Orders
Informal description
Let $\alpha$ be a type with a well-founded "greater than" relation $>$. For any element $a \in \alpha$ that is not minimal, there exists an element $a' \in \alpha$ such that $a'$ covers $a$ (denoted $a' \lessdot a$).