mk_preimage_equiv_lift — Mathlib

English

If f is a bijection (equivalence), then lift #(f^{-1} s) = lift # s.

Русский

Если f взаимно однозначное соответствие, то подъём кардинала прообраза равен подъёму кардинала самого множества.

LaTeX

$$$\\text{lift}(f^{-1}'s) = \\text{lift}(s)$$$

Lean4

@[simp]
theorem mk_preimage_equiv_lift {β : Type v} (f : α ≃ β) (s : Set β) : lift.{v} #(f ⁻¹' s) = lift.{u} #s :=
  by
  apply mk_preimage_of_injective_of_subset_range_lift _ _ f.injective
  rw [f.range_eq_univ]
  exact fun _ _ ↦ ⟨⟩

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