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

a ⩿ b = (a ≤ b ∧ ∀ ⦃c : α⦄, a < c → ¬c < b)

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 ≤ c → c ≤ b → c = 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 α] :

is_refl α wcovby

theorem wcovby.Ioo_eq {α : Type u_1} [preorder α] {a b : α} (h : a ⩿ b) :

set.Ioo a 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} [order_iso_class E α β] (e : E) :

⇑e a ⩿ ⇑e b ↔ 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 α} :

⇑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 to_dual_wcovby_to_dual_iff.

theorem wcovby.of_dual {α : Type u_1} [preorder α] {a b : order_dual α} :

b ⩿ a → ⇑order_dual.of_dual a ⩿ ⇑order_dual.of_dual b

Alias 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) :

c = a ∨ c = b

theorem wcovby.le_and_le_iff {α : Type u_1} [partial_order α] {a b c : α} (h : a ⩿ b) :

a ≤ c ∧ c ≤ b ↔ c = a ∨ c = b

theorem wcovby.Icc_eq {α : Type u_1} [partial_order α] {a b : α} (h : a ⩿ b) :

set.Icc a b = {a, b}

theorem wcovby.Ico_subset {α : Type u_1} [partial_order α] {a b : α} (h : a ⩿ b) :

set.Ico a b ⊆ {a}

theorem wcovby.Ioc_subset {α : Type u_1} [partial_order α] {a b : α} (h : a ⩿ b) :

set.Ioc a 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

a ⋖ b = (a < b ∧ ∀ ⦃c : α⦄, a < c → ¬c < b)

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 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 : α} [densely_ordered α] :

In a dense order, nothing covers anything.

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 α} :

⇑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 to_dual_covby_to_dual_iff.

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.

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 α] :

is_nonstrict_strict_order α wcovby covby

Equations

covby.is_nonstrict_strict_order = {right_iff_left_not_left := _}

@[protected, instance]

def covby.is_irrefl {α : Type u_1} [preorder α] :

is_irrefl α covby

theorem covby.Ioo_eq {α : Type u_1} [preorder α] {a b : α} (h : a ⋖ b) :

set.Ioo a 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} [order_iso_class E α β] (e : E) :

⇑e a ⋖ ⇑e b ↔ a ⋖ b

theorem wcovby.covby_of_ne {α : Type u_1} [partial_order α] {a b : α} (h : a ⩿ b) (h2 : a ≠ b) :

a ⋖ b

theorem covby_iff_wcovby_and_ne {α : Type u_1} [partial_order α] {a b : α} :

a ⋖ b ↔ a ⩿ b ∧ a ≠ b

theorem wcovby_iff_covby_or_eq {α : Type u_1} [partial_order α] {a b : α} :

a ⩿ b ↔ a ⋖ b ∨ a = b

theorem covby.Ico_eq {α : Type u_1} [partial_order α] {a b : α} (h : a ⋖ b) :

set.Ico a b = {a}

theorem covby.Ioc_eq {α : Type u_1} [partial_order α] {a b : α} (h : a ⋖ b) :

set.Ioc a b = {b}

theorem covby.Icc_eq {α : Type u_1} [partial_order α] {a b : α} (h : a ⋖ b) :

set.Icc a b = {a, b}

theorem set.wcovby_insert {α : Type u_1} (x : α) (s : set α) :

s ⩿ insert x s

theorem set.covby_insert {α : Type u_1} {x : α} {s : set α} (hx : x ∉ s) :

s ⋖ insert x s