mathlib documentation

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. ∃ b, a < b

Notation #

a ⋖ b means that b covers a.

source
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
source
theorem covby.lt {α : Type u_1} [has_lt α] {a b : α} (h : a ⋖ b) :
a < b
source
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.

source
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 not_covby_iff.

source
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.

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

In a dense order, nothing covers anything.

source
theorem densely_ordered_iff_forall_not_covby {α : Type u_1} [has_lt α] :
densely_ordered α ↔ ∀ (a b : α), ¬a ⋖ b
source
@[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
source
@[simp]
theorem of_dual_covby_of_dual_iff {α : Type u_1} [has_lt α] {a b : order_dual α} :
⇑order_dual.of_dual a ⋖ ⇑order_dual.of_dual b ↔ b ⋖ a
source
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 to_dual_covby_to_dual_iff.

source
theorem covby.of_dual {α : Type u_1} [has_lt α] {a b : order_dual α} :
b ⋖ a → ⇑order_dual.of_dual a ⋖ ⇑order_dual.of_dual b

Alias of of_dual_covby_of_dual_iff.

source
theorem covby.le {α : Type u_1} [preorder α] {a b : α} (h : a ⋖ b) :
a ≤ b
source
@[protected]
theorem covby.ne {α : Type u_1} [preorder α] {a b : α} (h : a ⋖ b) :
a ≠ b
source
theorem covby.ne' {α : Type u_1} [preorder α] {a b : α} (h : a ⋖ b) :
b ≠ a
source
@[protected, instance]
def covby.is_irrefl {α : Type u_1} [preorder α] :
is_irrefl α covby
source
theorem covby.Ioo_eq {α : Type u_1} [preorder α] {a b : α} (h : a ⋖ b) :
set.Ioo a b = ∅
source
theorem covby.of_image {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {a b : α} {f : α ↪o β} (h : ⇑f a ⋖ ⇑f b) :
a ⋖ b
source
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
source
@[protected]
theorem set.ord_connected.image_covby_image_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
source
@[simp]
theorem apply_covby_apply_iff {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {a b : α} {e : α ≃o β} :
⇑e a ⋖ ⇑e b ↔ a ⋖ b
source
theorem covby.Ico_eq {α : Type u_1} [partial_order α] {a b : α} (h : a ⋖ b) :
set.Ico a b = {a}
source
theorem covby.Ioc_eq {α : Type u_1} [partial_order α] {a b : α} (h : a ⋖ b) :
set.Ioc a b = {b}
source
theorem covby.Icc_eq {α : Type u_1} [partial_order α] {a b : α} (h : a ⋖ b) :
set.Icc a b = {a, b}