bounded_singleton — Mathlib

English

For any x, the singleton {x} is bounded with respect to r when α is well-ordered by r and type r is a succ-limit.

Русский

Для любого x множество {x} ограничено по r, когда α хорошо упорядочено по r и type r является succ-ограничением.

LaTeX

$$$$ \forall x,\; \mathrm{Bounded}_r(\{x\}) $$$$

Lean4

theorem bounded_singleton {r : α → α → Prop} [IsWellOrder α r] (hr : IsSuccLimit (type r)) (x) : Bounded r { x } :=
  by
  refine ⟨enum r ⟨succ (typein r x), hr.succ_lt (typein_lt_type r x)⟩, ?_⟩
  intro b hb
  rw [mem_singleton_iff.1 hb]
  nth_rw 1 [← enum_typein r x]
  rw [@enum_lt_enum _ r, Subtype.mk_lt_mk]
  apply lt_succ

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