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 thatb
coversa
.a ⩿ b
means thatb
weakly 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
.
@[simp]
theorem
apply_wcovby_apply_iff
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
{a b : α}
{E : Type u_3}
[order_iso_class E α β]
(e : E) :
@[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) :
Alias of the forward direction of not_covby_iff
.
Alias of exists_lt_lt_of_not_covby
.
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
.
@[simp]
theorem
apply_covby_apply_iff
{α : Type u_1}
{β : Type u_2}
[preorder α]
[preorder β]
{a b : α}
{E : Type u_3}
[order_iso_class E α β]
(e : E) :
theorem
wcovby.covby_of_ne
{α : Type u_1}
[partial_order α]
{a b : α}
(h : a ⩿ b)
(h2 : a ≠ b) :
a ⋖ b
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
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
prod.fst_eq_or_snd_eq_of_wcovby
{α : 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₂ : β} :