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 covers {α : Type u_1} [has_lt α] (a b : α) :
Prop

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

Equations
source
theorem covers.lt {α : Type u_1} [has_lt α] {a b : α} (h : a ⋖ b) :
a < b
source
theorem not_covers_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
@[simp]
theorem to_dual_covers_to_dual_iff {α : Type u_1} [has_lt α] {a b : α} :
⇑order_dual.to_dual b ⋖ ⇑order_dual.to_dual a ↔ a ⋖ b
source
theorem covers.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_covers_to_dual_iff.

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

In a dense order, nothing covers anything.

source
theorem covers.le {α : Type u_1} [preorder α] {a b : α} (h : a ⋖ b) :
a ≤ b
source
@[protected]
theorem covers.ne {α : Type u_1} [preorder α] {a b : α} (h : a ⋖ b) :
a ≠ b
source
theorem covers.ne' {α : Type u_1} [preorder α] {a b : α} (h : a ⋖ b) :
b ≠ a
source
theorem covers.Ioo_eq {α : Type u_1} [preorder α] {a b : α} (h : a ⋖ b) :
set.Ioo a b = ∅
source
@[protected, instance]
def covers.is_irrefl {α : Type u_1} [preorder α] :
is_irrefl α covers
source
theorem covers.Ico_eq {α : Type u_1} [partial_order α] {a b : α} (h : a ⋖ b) :
set.Ico a b = {a}
source
theorem covers.Ioc_eq {α : Type u_1} [partial_order α] {a b : α} (h : a ⋖ b) :
set.Ioc a b = {b}
source
theorem covers.Icc_eq {α : Type u_1} [partial_order α] {a b : α} (h : a ⋖ b) :
set.Icc a b = {a, b}