The covering relation #
This file proves properties of the covering relation in an order.
We say that b
covers 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
.
Alias of wcovBy_of_le_of_le
.
Alias of the reverse direction of toDual_wcovBy_toDual_iff
.
Alias of the reverse direction of ofDual_wcovBy_ofDual_iff
.
An iff
version of WCovBy.eq_or_eq
and wcovBy_of_eq_or_eq
.
Alias of the forward direction of not_covBy_iff
.
Alias of the forward direction of not_covBy_iff
.
If a < b
, then b
does not cover a
iff there's an element in between.
Alias of the reverse direction of toDual_covBy_toDual_iff
.
Alias of the reverse direction of ofDual_covBy_ofDual_iff
.
Alias of the forward direction of wcovBy_iff_covBy_or_eq
.
Alias of the forward direction of wcovBy_iff_eq_or_covBy
.
An iff
version of CovBy.eq_or_eq
and covBy_of_eq_or_eq
.
If a
, b
, c
are consecutive and a < x < c
then x = b
.
Alias of the forward direction of covBy_iff_lt_iff_le_left
.
Alias of the forward direction of covBy_iff_le_iff_lt_left
.
Alias of the forward direction of covBy_iff_lt_iff_le_right
.
Alias of the forward direction of covBy_iff_le_iff_lt_right
.
If a < b
then there exist a' > a
and b' < b
such that Set.Iio a'
is strictly to the left
of Set.Ioi b'
.
Equations
- x✝¹.instDecidableRelWCovBy x✝ = decidable_of_iff (x✝¹ ≤ x✝) ⋯
Equations
- x✝¹.instDecidableRelCovBy x✝ = decidable_of_iff (x✝¹ < x✝) ⋯