le_lift_iff — Mathlib

English

For a, b, we have b ≤ lift a if and only if there exists a' ≤ a with lift a' = b.

Русский

Для кардиналов a, b выполняется b ≤ lift a ⇔ существует a' ≤ a с lift a' = b.

LaTeX

$$$$ b \\le \\mathrm{lift}(a) \\iff \\exists a' \\le a, \\ \\mathrm{lift}(a') = b. $$$$

Lean4

theorem le_lift_iff {a : Cardinal.{u}} {b : Cardinal.{max u v}} : b ≤ lift.{v, u} a ↔ ∃ a' ≤ a, lift.{v, u} a' = b :=
  liftInitialSeg.le_apply_iff

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