type_lift_preimage — Mathlib

English

Lifting the type of a preimage under a bijection commutes with lift.

Русский

Поднятие типа предобраза через биекция сохраняется под лифтом.

LaTeX

$$$\\operatorname{lift}(\\mathrm{type}(f^{-1} o r)) = \\operatorname{lift}(\\mathrm{type}(r)).$$$

Lean4

@[simp]
theorem type_lift_preimage (r : α → α → Prop) [IsWellOrder α r] (f : β ≃ α) :
    lift.{u} (type (f ⁻¹'o r)) = lift.{v} (type r) :=
  (RelIso.preimage f r).ordinal_lift_type_eq

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