wellFoundedOn_lt — Mathlib

English

If a set s is bounded below in a preorder, then s endowed with the strict order < is a well-founded relation.

Русский

Если множество s ограничено снизу в пределе порядка, то множество s с отношением < образует хорошо основанный порядок.

LaTeX

$$BddBelow s \rightarrow s.WellFoundedOn (<)$$

Lean4

theorem wellFoundedOn_lt : BddBelow s → s.WellFoundedOn (· < ·) :=
  by
  rw [wellFoundedOn_iff_no_descending_seq]
  rintro ⟨a, ha⟩ f hf
  refine infinite_range_of_injective f.injective ?_
  exact
    (finite_Icc a <| f 0).subset <|
      range_subset_iff.2 <| fun n =>
        ⟨ha <| hf _, antitone_iff_forall_lt.2 (fun a b hab => (f.map_rel_iff.2 hab).le) <| Nat.zero_le _⟩

Похожие утверждения