mem_range_lift_of_card_le — Mathlib

English

If a cardinal a bounds the cardinality of an ordinal b in a lifted universe, then b belongs to the image of the lift map; i.e., there exists some c with lift(c) = b.

Русский

Если кардинал a ограничивает кардинальность ординала b в поднятой вселенной, то b лежит в образе отображения lift; существует c such that lift(c) = b.

LaTeX

$$$\forall a\in\mathrm{Cardinal},\forall b\in\mathrm{Ordinal},\; \operatorname{card}(b) \le \operatorname{lift}(a) \Rightarrow \exists c,\; \operatorname{lift}(c) = b$$$

Lean4

theorem mem_range_lift_of_card_le {a : Cardinal.{u}} {b : Ordinal.{max u v}} (h : card b ≤ Cardinal.lift.{v, u} a) :
    b ∈ Set.range lift.{v, u} := by
  rw [card_le_iff, ← lift_succ, ← lift_ord] at h
  exact mem_range_lift_of_le h.le

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