lift_pred — Mathlib

English

lifting commutes with pred: lift (pred o) = pred (lift o).

Русский

перекидка сохраняет пред: lift (pred o) = pred (lift o).

LaTeX

$$$$ \mathrm{lift}(\mathrm{pred}(o)) = \mathrm{pred}(\mathrm{lift}(o)) $$$$

Lean4

@[simp]
theorem lift_pred (o : Ordinal.{v}) : lift.{u} (pred o) = pred (lift.{u} o) :=
  by
  obtain ⟨a, rfl⟩ | ho := mem_range_succ_or_isSuccPrelimit o
  · simp
  · rwa [ho.ordinalPred_eq, eq_comm, pred_eq_iff_isSuccPrelimit, isSuccPrelimit_lift]

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