mk_image_le_lift — Mathlib

English

The lifted cardinality of the image is bounded by the lifted cardinality of the domain: lift(|f''s|) ≤ lift(|s|).

Русский

При переносе кардинальностей в более крупную вселенную, кардинальность образа не превосходит кардинальность исходного множества: lift(|f''s|) ≤ lift(|s|).

LaTeX

$$$\\mathrm{lift}\\,|f''s| \\le \\mathrm{lift}\\,|s|$$$

Lean4

theorem mk_image_le_lift {α : Type u} {β : Type v} {f : α → β} {s : Set α} : lift.{u} #(f '' s) ≤ lift.{v} #s :=
  lift_mk_le.{0}.mpr ⟨Embedding.ofSurjective _ imageFactorization_surjective⟩

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