English
If there exists a bijection between two sets s and t, then their finite cardinalities are equal: |s| = |t|.
Русский
Если существует биекция между множествами s и t, то их конечные кардинальности равны: |s| = |t|.
LaTeX
$$$$ \exists f: s \to t \text{ bijective} \Rightarrow |s| = |t| $$$$
Lean4
theorem ncard_eq_of_bijective {n : ℕ} (f : ∀ i, i < n → α) (hf : ∀ a ∈ s, ∃ i, ∃ h : i < n, f i h = a)
(hf' : ∀ (i) (h : i < n), f i h ∈ s) (f_inj : ∀ (i j) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j) :
s.ncard = n := by
let f' : Fin n → α := fun i ↦ f i.val i.is_lt
suffices himage : s = f' '' Set.univ
by
rw [← Fintype.card_fin n, ← Nat.card_eq_fintype_card, ← Set.ncard_univ, himage]
exact ncard_image_of_injOn <| fun i _hi j _hj h ↦ Fin.ext <| f_inj i.val j.val i.is_lt j.is_lt h
ext x
simp only [image_univ, mem_range]
refine ⟨fun hx ↦ ?_, fun ⟨⟨i, hi⟩, hx⟩ ↦ hx ▸ hf' i hi⟩
obtain ⟨i, hi, rfl⟩ := hf x hx
use ⟨i, hi⟩
