exists_bijOn_of_encard_eq — Mathlib

English

If s is finite and s.encard = t.encard, there exists f with BijOn f s t.

Русский

Если s конечно и encard равна encard t, существует биекция f между s и t.

LaTeX

$$$\\exists f : \\alpha \\to \\beta, BijOn f s t$$$

Lean4

theorem exists_bijOn_of_encard_eq [Nonempty β] (hs : s.Finite) (h : s.encard = t.encard) : ∃ (f : α → β), BijOn f s t :=
  by
  obtain ⟨f, hf, hinj⟩ := hs.exists_injOn_of_encard_le h.le; use f
  convert hinj.bijOn_image
  rw [(hs.image f).eq_of_subset_of_encard_le (image_subset_iff.mpr hf) (h.symm.trans hinj.encard_image.symm).le]

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