mathlib3 documentation

order.succ_pred.limit

Successor and predecessor limits #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We define the predicate order.is_succ_limit for "successor limits", values that don't cover any others. They are so named since they can't be the successors of anything smaller. We define order.is_pred_limit analogously, and prove basic results.

Todo #

The plan is to eventually replace ordinal.is_limit and cardinal.is_limit with the common predicate order.is_succ_limit.

Successor limits #

source
def order.is_succ_limit {α : Type u_1} [has_lt α] (a : α) :
Prop

A successor limit is a value that doesn't cover any other.

It's so named because in a successor order, a successor limit can't be the successor of anything smaller.

Equations
source
theorem order.not_is_succ_limit_iff_exists_covby {α : Type u_1} [has_lt α] (a : α) :
¬order.is_succ_limit a ↔ ∃ (b : α), b ⋖ a
source
@[simp]
theorem order.is_succ_limit_of_dense {α : Type u_1} [has_lt α] [densely_ordered α] (a : α) :
order.is_succ_limit a
source
@[protected]
theorem is_min.is_succ_limit {α : Type u_1} [preorder α] {a : α} :
is_min a → order.is_succ_limit a
source
theorem order.is_succ_limit_bot {α : Type u_1} [preorder α] [order_bot α] :
order.is_succ_limit ⊥
source
@[protected]
theorem order.is_succ_limit.is_max {α : Type u_1} [preorder α] {a : α} [succ_order α] (h : order.is_succ_limit (order.succ a)) :
is_max a
source
theorem order.not_is_succ_limit_succ_of_not_is_max {α : Type u_1} [preorder α] {a : α} [succ_order α] (ha : ¬is_max a) :
¬order.is_succ_limit (order.succ a)
source
theorem order.is_succ_limit.succ_ne {α : Type u_1} [preorder α] {a : α} [succ_order α] [no_max_order α] (h : order.is_succ_limit a) (b : α) :
order.succ b ≠ a
source
@[simp]
theorem order.not_is_succ_limit_succ {α : Type u_1} [preorder α] [succ_order α] [no_max_order α] (a : α) :
¬order.is_succ_limit (order.succ a)
source
theorem order.is_succ_limit.is_min_of_no_max {α : Type u_1} [preorder α] {a : α} [succ_order α] [is_succ_archimedean α] [no_max_order α] (h : order.is_succ_limit a) :
is_min a
source
@[simp]
theorem order.is_succ_limit_iff_of_no_max {α : Type u_1} [preorder α] {a : α} [succ_order α] [is_succ_archimedean α] [no_max_order α] :
order.is_succ_limit a ↔ is_min a
source
theorem order.not_is_succ_limit_of_no_max {α : Type u_1} [preorder α] {a : α} [succ_order α] [is_succ_archimedean α] [no_min_order α] [no_max_order α] :
¬order.is_succ_limit a
source
theorem order.is_succ_limit_of_succ_ne {α : Type u_1} [partial_order α] [succ_order α] {a : α} (h : ∀ (b : α), order.succ b ≠ a) :
order.is_succ_limit a
source
theorem order.not_is_succ_limit_iff {α : Type u_1} [partial_order α] [succ_order α] {a : α} :
¬order.is_succ_limit a ↔ ∃ (b : α), ¬is_max b ∧ order.succ b = a
source
theorem order.mem_range_succ_of_not_is_succ_limit {α : Type u_1} [partial_order α] [succ_order α] {a : α} (h : ¬order.is_succ_limit a) :
a ∈ set.range order.succ

See not_is_succ_limit_iff for a version that states that a is a successor of a value other than itself.

source
theorem order.is_succ_limit_of_succ_lt {α : Type u_1} [partial_order α] [succ_order α] {b : α} (H : ∀ (a : α), a < b → order.succ a < b) :
order.is_succ_limit b
source
theorem order.is_succ_limit.succ_lt {α : Type u_1} [partial_order α] [succ_order α] {a b : α} (hb : order.is_succ_limit b) (ha : a < b) :
order.succ a < b
source
theorem order.is_succ_limit.succ_lt_iff {α : Type u_1} [partial_order α] [succ_order α] {a b : α} (hb : order.is_succ_limit b) :
order.succ a < b ↔ a < b
source
theorem order.is_succ_limit_iff_succ_lt {α : Type u_1} [partial_order α] [succ_order α] {b : α} :
order.is_succ_limit b ↔ ∀ (a : α), a < b → order.succ a < b
source
noncomputable def order.is_succ_limit_rec_on {α : Type u_1} [partial_order α] [succ_order α] {C : α → Sort u_2} (b : α) (hs : Π (a : α), ¬is_max a → C (order.succ a)) (hl : Π (a : α), order.is_succ_limit a → C a) :
C b

A value can be built by building it on successors and successor limits.

Equations
source
theorem order.is_succ_limit_rec_on_limit {α : Type u_1} [partial_order α] [succ_order α] {b : α} {C : α → Sort u_2} (hs : Π (a : α), ¬is_max a → C (order.succ a)) (hl : Π (a : α), order.is_succ_limit a → C a) (hb : order.is_succ_limit b) :
order.is_succ_limit_rec_on b hs hl = hl b hb
source
theorem order.is_succ_limit_rec_on_succ' {α : Type u_1} [partial_order α] [succ_order α] {C : α → Sort u_2} (hs : Π (a : α), ¬is_max a → C (order.succ a)) (hl : Π (a : α), order.is_succ_limit a → C a) {b : α} (hb : ¬is_max b) :
order.is_succ_limit_rec_on (order.succ b) hs hl = hs b hb
source
@[simp]
theorem order.is_succ_limit_rec_on_succ {α : Type u_1} [partial_order α] [succ_order α] {C : α → Sort u_2} [no_max_order α] (hs : Π (a : α), ¬is_max a → C (order.succ a)) (hl : Π (a : α), order.is_succ_limit a → C a) (b : α) :
order.is_succ_limit_rec_on (order.succ b) hs hl = hs b _
source
theorem order.is_succ_limit_iff_succ_ne {α : Type u_1} [partial_order α] [succ_order α] {a : α} [no_max_order α] :
order.is_succ_limit a ↔ ∀ (b : α), order.succ b ≠ a
source
theorem order.not_is_succ_limit_iff' {α : Type u_1} [partial_order α] [succ_order α] {a : α} [no_max_order α] :
¬order.is_succ_limit a ↔ a ∈ set.range order.succ
source
@[protected]
theorem order.is_succ_limit.is_min {α : Type u_1} [partial_order α] [succ_order α] {a : α} [is_succ_archimedean α] (h : order.is_succ_limit a) :
is_min a
source
@[simp]
theorem order.is_succ_limit_iff {α : Type u_1} [partial_order α] [succ_order α] {a : α} [is_succ_archimedean α] :
order.is_succ_limit a ↔ is_min a
source
theorem order.not_is_succ_limit {α : Type u_1} [partial_order α] [succ_order α] {a : α} [is_succ_archimedean α] [no_min_order α] :
¬order.is_succ_limit a

Predecessor limits #

source
def order.is_pred_limit {α : Type u_1} [has_lt α] (a : α) :
Prop

A predecessor limit is a value that isn't covered by any other.

It's so named because in a predecessor order, a predecessor limit can't be the predecessor of anything greater.

Equations
source
theorem order.not_is_pred_limit_iff_exists_covby {α : Type u_1} [has_lt α] (a : α) :
¬order.is_pred_limit a ↔ ∃ (b : α), a ⋖ b
source
theorem order.is_pred_limit_of_dense {α : Type u_1} [has_lt α] [densely_ordered α] (a : α) :
order.is_pred_limit a
source
@[simp]
theorem order.is_succ_limit_to_dual_iff {α : Type u_1} [has_lt α] {a : α} :
order.is_succ_limit (⇑order_dual.to_dual a) ↔ order.is_pred_limit a
source
@[simp]
theorem order.is_pred_limit_to_dual_iff {α : Type u_1} [has_lt α] {a : α} :
order.is_pred_limit (⇑order_dual.to_dual a) ↔ order.is_succ_limit a
source
theorem order.is_pred_limit.dual {α : Type u_1} [has_lt α] {a : α} :
order.is_pred_limit a → order.is_succ_limit (⇑order_dual.to_dual a)

Alias of the reverse direction of order.is_succ_limit_to_dual_iff.

source
theorem order.is_succ_limit.dual {α : Type u_1} [has_lt α] {a : α} :
order.is_succ_limit a → order.is_pred_limit (⇑order_dual.to_dual a)

Alias of the reverse direction of order.is_pred_limit_to_dual_iff.

source
@[protected]
theorem is_max.is_pred_limit {α : Type u_1} [preorder α] {a : α} :
is_max a → order.is_pred_limit a
source
theorem order.is_pred_limit_top {α : Type u_1} [preorder α] [order_top α] :
order.is_pred_limit ⊤
source
@[protected]
theorem order.is_pred_limit.is_min {α : Type u_1} [preorder α] {a : α} [pred_order α] (h : order.is_pred_limit (order.pred a)) :
is_min a
source
theorem order.not_is_pred_limit_pred_of_not_is_min {α : Type u_1} [preorder α] {a : α} [pred_order α] (ha : ¬is_min a) :
¬order.is_pred_limit (order.pred a)
source
theorem order.is_pred_limit.pred_ne {α : Type u_1} [preorder α] {a : α} [pred_order α] [no_min_order α] (h : order.is_pred_limit a) (b : α) :
order.pred b ≠ a
source
@[simp]
theorem order.not_is_pred_limit_pred {α : Type u_1} [preorder α] [pred_order α] [no_min_order α] (a : α) :
¬order.is_pred_limit (order.pred a)
source
@[protected]
theorem order.is_pred_limit.is_max_of_no_min {α : Type u_1} [preorder α] {a : α} [pred_order α] [is_pred_archimedean α] [no_min_order α] (h : order.is_pred_limit a) :
is_max a
source
@[simp]
theorem order.is_pred_limit_iff_of_no_min {α : Type u_1} [preorder α] {a : α} [pred_order α] [is_pred_archimedean α] [no_min_order α] :
order.is_pred_limit a ↔ is_max a
source
theorem order.not_is_pred_limit_of_no_min {α : Type u_1} [preorder α] {a : α} [pred_order α] [is_pred_archimedean α] [no_min_order α] [no_max_order α] :
¬order.is_pred_limit a
source
theorem order.is_pred_limit_of_pred_ne {α : Type u_1} [partial_order α] [pred_order α] {a : α} (h : ∀ (b : α), order.pred b ≠ a) :
order.is_pred_limit a
source
theorem order.not_is_pred_limit_iff {α : Type u_1} [partial_order α] [pred_order α] {a : α} :
¬order.is_pred_limit a ↔ ∃ (b : α), ¬is_min b ∧ order.pred b = a
source
theorem order.mem_range_pred_of_not_is_pred_limit {α : Type u_1} [partial_order α] [pred_order α] {a : α} (h : ¬order.is_pred_limit a) :
a ∈ set.range order.pred

See not_is_pred_limit_iff for a version that states that a is a successor of a value other than itself.

source
theorem order.is_pred_limit_of_pred_lt {α : Type u_1} [partial_order α] [pred_order α] {b : α} (H : ∀ (a : α), a > b → order.pred a < b) :
order.is_pred_limit b
source
theorem order.is_pred_limit.lt_pred {α : Type u_1} [partial_order α] [pred_order α] {a b : α} (h : order.is_pred_limit a) :
a < b → a < order.pred b
source
theorem order.is_pred_limit.lt_pred_iff {α : Type u_1} [partial_order α] [pred_order α] {a b : α} (h : order.is_pred_limit a) :
a < order.pred b ↔ a < b
source
theorem order.is_pred_limit_iff_lt_pred {α : Type u_1} [partial_order α] [pred_order α] {a : α} :
order.is_pred_limit a ↔ ∀ ⦃b : α⦄, a < b → a < order.pred b
source
noncomputable def order.is_pred_limit_rec_on {α : Type u_1} [partial_order α] [pred_order α] {C : α → Sort u_2} (b : α) (hs : Π (a : α), ¬is_min a → C (order.pred a)) (hl : Π (a : α), order.is_pred_limit a → C a) :
C b

A value can be built by building it on predecessors and predecessor limits.

Equations
source
theorem order.is_pred_limit_rec_on_limit {α : Type u_1} [partial_order α] [pred_order α] {b : α} {C : α → Sort u_2} (hs : Π (a : α), ¬is_min a → C (order.pred a)) (hl : Π (a : α), order.is_pred_limit a → C a) (hb : order.is_pred_limit b) :
order.is_pred_limit_rec_on b hs hl = hl b hb
source
theorem order.is_pred_limit_rec_on_pred' {α : Type u_1} [partial_order α] [pred_order α] {C : α → Sort u_2} (hs : Π (a : α), ¬is_min a → C (order.pred a)) (hl : Π (a : α), order.is_pred_limit a → C a) {b : α} (hb : ¬is_min b) :
order.is_pred_limit_rec_on (order.pred b) hs hl = hs b hb
source
@[simp]
theorem order.is_pred_limit_rec_on_pred {α : Type u_1} [partial_order α] [pred_order α] {C : α → Sort u_2} [no_min_order α] (hs : Π (a : α), ¬is_min a → C (order.pred a)) (hl : Π (a : α), order.is_pred_limit a → C a) (b : α) :
order.is_pred_limit_rec_on (order.pred b) hs hl = hs b _
source
@[protected]
theorem order.is_pred_limit.is_max {α : Type u_1} [partial_order α] [pred_order α] {a : α} [is_pred_archimedean α] (h : order.is_pred_limit a) :
is_max a
source
@[simp]
theorem order.is_pred_limit_iff {α : Type u_1} [partial_order α] [pred_order α] {a : α} [is_pred_archimedean α] :
order.is_pred_limit a ↔ is_max a
source
theorem order.not_is_pred_limit {α : Type u_1} [partial_order α] [pred_order α] {a : α} [is_pred_archimedean α] [no_max_order α] :
¬order.is_pred_limit a