The covering relation #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 ⋖ bmeans thatbcoversa.a ⩿ bmeans thatbweakly coversa.
theorem
has_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
antisymm_rel.wcovby
{α : Type u_1}
[preorder α]
{a b : α}
(h : antisymm_rel has_le.le a b) :
a ⩿ b
theorem
antisymm_rel.trans_wcovby
{α : Type u_1}
[preorder α]
{a b c : α}
(hab : antisymm_rel has_le.le a b)
(hbc : b ⩿ c) :
a ⩿ c
theorem
wcovby_congr_left
{α : Type u_1}
[preorder α]
{a b c : α}
(hab : antisymm_rel has_le.le a b) :
theorem
wcovby.trans_antisymm_rel
{α : Type u_1}
[preorder α]
{a b c : α}
(hab : a ⩿ b)
(hbc : antisymm_rel has_le.le b c) :
a ⩿ c
theorem
wcovby_congr_right
{α : Type u_1}
[preorder α]
{a b c : α}
(hab : antisymm_rel has_le.le a b) :
@[simp]
theorem
to_dual_wcovby_to_dual_iff
{α : Type u_1}
[preorder α]
{a b : α} :
⇑order_dual.to_dual b ⩿ ⇑order_dual.to_dual a ↔ a ⩿ b
@[simp]
theorem
of_dual_wcovby_of_dual_iff
{α : Type u_1}
[preorder α]
{a b : αᵒᵈ} :
⇑order_dual.of_dual a ⩿ ⇑order_dual.of_dual b ↔ b ⩿ a
theorem
wcovby.to_dual
{α : Type u_1}
[preorder α]
{a b : α} :
a ⩿ b → ⇑order_dual.to_dual b ⩿ ⇑order_dual.to_dual a
Alias of the reverse direction of to_dual_wcovby_to_dual_iff.
theorem
wcovby.of_dual
{α : Type u_1}
[preorder α]
{a b : αᵒᵈ} :
b ⩿ a → ⇑order_dual.of_dual a ⩿ ⇑order_dual.of_dual b
Alias of the reverse direction of of_dual_wcovby_of_dual_iff.
theorem
wcovby.eq_or_eq
{α : Type u_1}
[partial_order α]
{a b c : α}
(h : a ⩿ b)
(h2 : a ≤ c)
(h3 : c ≤ b) :
An iff version of wcovby.eq_or_eq and wcovby_of_eq_or_eq.
theorem
wcovby.sup_eq
{α : Type u_1}
[semilattice_sup α]
{a b c : α}
(hac : a ⩿ c)
(hbc : b ⩿ c)
(hab : a ≠ b) :
theorem
wcovby.inf_eq
{α : Type u_1}
[semilattice_inf α]
{a b c : α}
(hca : c ⩿ a)
(hcb : c ⩿ b)
(hab : a ≠ b) :
theorem
densely_ordered_iff_forall_not_covby
{α : Type u_1}
[has_lt α] :
densely_ordered α ↔ ∀ (a b : α), ¬a ⋖ b
@[simp]
theorem
to_dual_covby_to_dual_iff
{α : Type u_1}
[has_lt α]
{a b : α} :
⇑order_dual.to_dual b ⋖ ⇑order_dual.to_dual a ↔ a ⋖ b
@[simp]
theorem
of_dual_covby_of_dual_iff
{α : Type u_1}
[has_lt α]
{a b : αᵒᵈ} :
⇑order_dual.of_dual a ⋖ ⇑order_dual.of_dual b ↔ b ⋖ a
theorem
covby.to_dual
{α : Type u_1}
[has_lt α]
{a b : α} :
a ⋖ b → ⇑order_dual.to_dual b ⋖ ⇑order_dual.to_dual a
Alias of the reverse direction of to_dual_covby_to_dual_iff.
theorem
covby.of_dual
{α : Type u_1}
[has_lt α]
{a b : αᵒᵈ} :
b ⋖ a → ⇑order_dual.of_dual a ⋖ ⇑order_dual.of_dual b
Alias of the reverse direction of of_dual_covby_of_dual_iff.
theorem
antisymm_rel.trans_covby
{α : Type u_1}
[preorder α]
{a b c : α}
(hab : antisymm_rel has_le.le a b)
(hbc : b ⋖ c) :
a ⋖ c
theorem
covby_congr_left
{α : Type u_1}
[preorder α]
{a b c : α}
(hab : antisymm_rel has_le.le a b) :
theorem
covby.trans_antisymm_rel
{α : Type u_1}
[preorder α]
{a b c : α}
(hab : a ⋖ b)
(hbc : antisymm_rel has_le.le b c) :
a ⋖ c
theorem
covby_congr_right
{α : Type u_1}
[preorder α]
{a b c : α}
(hab : antisymm_rel has_le.le a b) :
theorem
wcovby.covby_of_ne
{α : Type u_1}
[partial_order α]
{a b : α}
(h : a ⩿ b)
(h2 : a ≠ b) :
a ⋖ b
Alias of the forward direction of wcovby_iff_covby_or_eq.
Alias of the forward direction of wcovby_iff_eq_or_covby.
theorem
covby.eq_or_eq
{α : Type u_1}
[partial_order α]
{a b c : α}
(h : a ⋖ b)
(h2 : a ≤ c)
(h3 : c ≤ b) :
An iff version of covby.eq_or_eq and covby_of_eq_or_eq.
theorem
wcovby.le_of_lt
{α : Type u_1}
[linear_order α]
{a b c : α}
(hab : a ⩿ b)
(hcb : c < b) :
c ≤ a
theorem
wcovby.ge_of_gt
{α : Type u_1}
[linear_order α]
{a b c : α}
(hab : a ⩿ b)
(hac : a < c) :
b ≤ c
theorem
covby.unique_left
{α : Type u_1}
[linear_order α]
{a b c : α}
(ha : a ⋖ c)
(hb : b ⋖ c) :
a = b
theorem
covby.unique_right
{α : Type u_1}
[linear_order α]
{a b c : α}
(hb : a ⋖ b)
(hc : a ⋖ c) :
b = c
theorem
covby.eq_of_between
{α : Type u_1}
[linear_order α]
{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
set.covby_insert
{α : Type u_1}
{x : α}
{s : set α}
(hx : x ∉ s) :
s ⋖ has_insert.insert x s
@[simp]
theorem
prod.swap_wcovby_swap
{α : Type u_1}
{β : Type u_2}
[partial_order α]
[partial_order β]
{x y : α × β} :
@[simp]
theorem
prod.swap_covby_swap
{α : Type u_1}
{β : Type u_2}
[partial_order α]
[partial_order β]
{x y : α × β} :
theorem
wcovby.fst
{α : Type u_1}
{β : Type u_2}
[partial_order α]
[partial_order β]
{x y : α × β}
(h : x ⩿ y) :
theorem
wcovby.snd
{α : Type u_1}
{β : Type u_2}
[partial_order α]
[partial_order β]
{x y : α × β}
(h : x ⩿ y) :
theorem
prod.mk_wcovby_mk_iff_left
{α : Type u_1}
{β : Type u_2}
[partial_order α]
[partial_order β]
{a₁ a₂ : α}
{b : β} :
theorem
prod.mk_wcovby_mk_iff_right
{α : Type u_1}
{β : Type u_2}
[partial_order α]
[partial_order β]
{a : α}
{b₁ b₂ : β} :
theorem
prod.mk_covby_mk_iff_left
{α : Type u_1}
{β : Type u_2}
[partial_order α]
[partial_order β]
{a₁ a₂ : α}
{b : β} :
theorem
prod.mk_covby_mk_iff_right
{α : Type u_1}
{β : Type u_2}
[partial_order α]
[partial_order β]
{a : α}
{b₁ b₂ : β} :
theorem
prod.mk_wcovby_mk_iff
{α : Type u_1}
{β : Type u_2}
[partial_order α]
[partial_order β]
{a₁ a₂ : α}
{b₁ b₂ : β} :
theorem
prod.mk_covby_mk_iff
{α : Type u_1}
{β : Type u_2}
[partial_order α]
[partial_order β]
{a₁ a₂ : α}
{b₁ b₂ : β} :