English
If there is a bijection between two sets, then their finite cardinalities are equal. In particular, if there is a bijection f' : s → t, then s.ncard = t.ncard.
Русский
Если существует биекция между двумя множествами, то их конечные кардинальности равны. В частности, если существует биекция f' : s → t, то s.ncard = t.ncard.
LaTeX
$$$$ \exists f: s \to t\text{ bijective} \Rightarrow s.ncard = t.ncard $$$$
Lean4
theorem ncard_congr {t : Set β} (f : ∀ a ∈ s, β) (h₁ : ∀ a ha, f a ha ∈ t) (h₂ : ∀ a b ha hb, f a ha = f b hb → a = b)
(h₃ : ∀ b ∈ t, ∃ a ha, f a ha = b) : s.ncard = t.ncard :=
by
set f' : s → t := fun x ↦ ⟨f x.1 x.2, h₁ _ _⟩
have hbij : f'.Bijective := by
constructor
· rintro ⟨x, hx⟩ ⟨y, hy⟩ hxy
simp only [f', Subtype.mk.injEq] at hxy ⊢
exact h₂ _ _ hx hy hxy
rintro ⟨y, hy⟩
obtain ⟨a, ha, rfl⟩ := h₃ y hy
simp only [Subtype.exists]
exact ⟨_, ha, rfl⟩
simp_rw [← _root_.Nat.card_coe_set_eq]
exact Nat.card_congr (Equiv.ofBijective f' hbij)
