has_succ_of_type_succ_lt — Mathlib

English

In a well-ordered α by r, for every x there exists a y with r x y.

Русский

В хорошо упорядоченном по r множестве для каждого x существует y с r x y.

LaTeX

$$$$ \forall x,\; \exists y,\; r(x,y) $$$$

Lean4

theorem has_succ_of_type_succ_lt {α} {r : α → α → Prop} [wo : IsWellOrder α r] (h : ∀ a < type r, succ a < type r)
    (x : α) : ∃ y, r x y := by
  use enum r ⟨succ (typein r x), h _ (typein_lt_type r x)⟩
  convert enum_lt_enum.mpr _
  · rw [enum_typein]
  · rw [Subtype.mk_lt_mk, lt_succ_iff]

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