lift_succ — Mathlib

English

Lifting preserves the successor: for any cardinal a, lift(succ(a)) = succ(lift(a)).

Русский

Возведение сохраняет переход к successor: lift(succ(a)) = succ(lift(a)).

LaTeX

$$$\\operatorname{lift}(\\operatorname{succ}(a)) = \\operatorname{succ}(\\operatorname{lift}(a))$$$

Lean4

@[simp]
theorem lift_succ (a) : lift.{v, u} (succ a) = succ (lift.{v, u} a) :=
  le_antisymm
    (le_of_not_gt fun h => by
      rcases lt_lift_iff.1 h with ⟨b, h, e⟩
      rw [lt_succ_iff, ← lift_le, e] at h
      exact h.not_gt (lt_succ _))
    (succ_le_of_lt <| lift_lt.2 <| lt_succ a)

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