order.cover

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
Instances for wcovby
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
@[protected]
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 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 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 cc bc = a c = b) :
a ⩿ 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.

@[protected, instance]
def wcovby.is_refl {α : Type u_1} [preorder α] :
theorem wcovby.Ioo_eq {α : Type u_1} [preorder α] {a b : α} (h : a ⩿ b) :
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.range f).ord_connected) :
f a ⩿ f b
theorem set.ord_connected.apply_wcovby_apply_iff {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {a b : α} (f : α ↪o β) (h : (set.range f).ord_connected) :
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} [ β] (e : E) :
e a ⩿ e b a ⩿ b
@[simp]
theorem to_dual_wcovby_to_dual_iff {α : Type u_1} [preorder α] {a b : α} :
@[simp]
theorem of_dual_wcovby_of_dual_iff {α : Type u_1} [preorder α] {a b : αᵒᵈ} :
theorem wcovby.to_dual {α : Type u_1} [preorder α] {a b : α} :
a ⩿ b

Alias of the reverse direction of to_dual_wcovby_to_dual_iff.

theorem wcovby.of_dual {α : Type u_1} [preorder α] {a b : αᵒᵈ} :
b ⩿ a

Alias of the reverse direction of of_dual_wcovby_of_dual_iff.

theorem wcovby.eq_or_eq {α : Type u_1} {a b c : α} (h : a ⩿ b) (h2 : a c) (h3 : c b) :
c = a c = b
theorem wcovby.le_and_le_iff {α : Type u_1} {a b c : α} (h : a ⩿ b) :
a c c b c = a c = b
theorem wcovby.Icc_eq {α : Type u_1} {a b : α} (h : a ⩿ b) :
b = {a, b}
theorem wcovby.Ico_subset {α : Type u_1} {a b : α} (h : a ⩿ b) :
b {a}
theorem wcovby.Ioc_subset {α : Type u_1} {a b : α} (h : a ⩿ b) :
b {b}
def covby {α : Type u_1} [has_lt α] (a b : α) :
Prop

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

Equations
Instances for covby
theorem covby.lt {α : Type u_1} [has_lt α] {a b : α} (h : a b) :
a < b
theorem not_covby_iff {α : Type u_1} [has_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} [has_lt α] {a b : α} (h : a < b) :
¬a b(∃ (c : α), a < c c < b)

Alias of the forward direction of not_covby_iff.

theorem has_lt.lt.exists_lt_lt {α : Type u_1} [has_lt α] {a b : α} (h : a < b) :
¬a b(∃ (c : α), a < c c < b)

Alias of exists_lt_lt_of_not_covby.

theorem not_covby {α : Type u_1} [has_lt α] {a b : α}  :
¬a b

In a dense order, nothing covers anything.

theorem densely_ordered_iff_forall_not_covby {α : Type u_1} [has_lt α] :
∀ (a b : α), ¬a b
@[simp]
theorem to_dual_covby_to_dual_iff {α : Type u_1} [has_lt α] {a b : α} :
@[simp]
theorem of_dual_covby_of_dual_iff {α : Type u_1} [has_lt α] {a b : αᵒᵈ} :
theorem covby.to_dual {α : Type u_1} [has_lt α] {a b : α} :
a b

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

Alias of the reverse direction of of_dual_covby_of_dual_iff.

theorem covby.le {α : Type u_1} [preorder α] {a b : α} (h : a b) :
a b
@[protected]
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
@[protected]
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_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
@[protected, instance]
def covby.is_nonstrict_strict_order {α : Type u_1} [preorder α] :
Equations
@[protected, instance]
def covby.is_irrefl {α : Type u_1} [preorder α] :
theorem covby.Ioo_eq {α : Type u_1} [preorder α] {a b : α} (h : a b) :
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.range f).ord_connected) :
f a f b
theorem set.ord_connected.apply_covby_apply_iff {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {a b : α} (f : α ↪o β) (h : (set.range f).ord_connected) :
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} [ β] (e : E) :
e a e b a b
theorem wcovby.covby_of_ne {α : Type u_1} {a b : α} (h : a ⩿ b) (h2 : a b) :
a b
theorem covby_iff_wcovby_and_ne {α : Type u_1} {a b : α} :
a b a ⩿ b a b
theorem wcovby_iff_covby_or_eq {α : Type u_1} {a b : α} :
a ⩿ b a b a = b
theorem covby.Ico_eq {α : Type u_1} {a b : α} (h : a b) :
b = {a}
theorem covby.Ioc_eq {α : Type u_1} {a b : α} (h : a b) :
b = {b}
theorem covby.Icc_eq {α : Type u_1} {a b : α} (h : a b) :
b = {a, b}
theorem covby.Ioi_eq {α : Type u_1} [linear_order α] {a b : α} (h : a b) :
=
theorem covby.Iio_eq {α : Type u_1} [linear_order α] {a b : α} (h : 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.le_of_lt {α : Type u_1} [linear_order α] {a b c : α} (hab : a b) :
c < bc a
theorem covby.ge_of_gt {α : Type u_1} [linear_order α] {a b c : α} (hab : a b) :
a < cb 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.wcovby_insert {α : Type u_1} (x : α) (s : set α) :
s ⩿
theorem set.covby_insert {α : Type u_1} {x : α} {s : set α} (hx : x s) :
s
@[simp]
theorem prod.swap_wcovby_swap {α : Type u_1} {β : Type u_2} {x y : α × β} :
x.swap ⩿ y.swap x ⩿ y
@[simp]
theorem prod.swap_covby_swap {α : Type u_1} {β : Type u_2} {x y : α × β} :
x.swap y.swap x y
theorem prod.fst_eq_or_snd_eq_of_wcovby {α : Type u_1} {β : Type u_2} {x y : α × β} :
x ⩿ yx.fst = y.fst x.snd = y.snd
theorem wcovby.fst {α : Type u_1} {β : Type u_2} {x y : α × β} (h : x ⩿ y) :
x.fst ⩿ y.fst
theorem wcovby.snd {α : Type u_1} {β : Type u_2} {x y : α × β} (h : x ⩿ y) :
x.snd ⩿ y.snd
theorem prod.mk_wcovby_mk_iff_left {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} {b : β} :
(a₁, b) ⩿ (a₂, b) a₁ ⩿ a₂
theorem prod.mk_wcovby_mk_iff_right {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} :
(a, b₁) ⩿ (a, b₂) b₁ ⩿ b₂
theorem prod.mk_covby_mk_iff_left {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} {b : β} :
(a₁, b) (a₂, b) a₁ a₂
theorem prod.mk_covby_mk_iff_right {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} :
(a, b₁) (a, b₂) b₁ b₂
theorem prod.mk_wcovby_mk_iff {α : Type u_1} {β : Type u_2} {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} {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} {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} {x y : α × β} :
x y x.fst y.fst x.snd = y.snd x.snd y.snd x.fst = y.fst