mk_preimage_of_injective — Mathlib

English

If f is injective and s ⊆ range f, then lift #(f^{-1}' s) = lift # s.

Русский

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

LaTeX

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

Lean4

theorem mk_preimage_of_injective (f : α → β) (s : Set β) (h : Injective f) : #(f ⁻¹' s) ≤ #s :=
  by
  rw [← lift_id #(↑(f ⁻¹' s)), ← lift_id #(↑s)]
  exact mk_preimage_of_injective_lift f s h

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