card_typein_lt — Mathlib

English

If α is well-ordered by r and x ∈ α, and ord(#α) = type r, then card(typein r x) < #α.

Русский

Пусть α упорядочено отношением r и x ∈ α; если ord(#α) = type r, то card(typein r x) < #α.

LaTeX

$$$ \operatorname{ord}(\#\alpha) = \operatorname{type}(r) \implies \operatorname{card}(\operatorname{typein}(r,x)) < \#\alpha $$$

Lean4

theorem card_typein_lt (r : α → α → Prop) [IsWellOrder α r] (x : α) (h : ord #α = type r) : card (typein r x) < #α :=
  by
  rw [← lt_ord, h]
  apply typein_lt_type

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