mk_preimage_of_injective_lift — Mathlib

English

If f is injective, then |f^{-1}(S)| ≤ |S| after lifting to the appropriate universe.

Русский

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

LaTeX

$$$|f^{-1}(S)| \\le |S|$$$

Lean4

theorem mk_preimage_of_injective_lift {α : Type u} {β : Type v} (f : α → β) (s : Set β) (h : Injective f) :
    lift.{v} #(f ⁻¹' s) ≤ lift.{u} #s := by
  rw [lift_mk_le.{0}]
  use Subtype.coind (fun x => f x.1) fun x => mem_preimage.mp x.2
  apply Subtype.coind_injective; exact h.comp Subtype.val_injective

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