nat_lt_lift_iff — Mathlib

English

For every natural number n and cardinal a, n is less than the lifted cardinal a if and only if n is less than a.

Русский

Для каждого натурального числа n и кардинала a верно, что n < lift(a) тогда и только тогда, когда n < a.

LaTeX

$$$n < \operatorname{lift}(a) \iff n < a$$$

Lean4

@[simp]
theorem nat_lt_lift_iff {n : ℕ} {a : Cardinal.{u}} : n < lift.{v} a ↔ n < a := by rw [← lift_natCast.{v, u}, lift_lt]

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