English
If there is a bijection between s and t that respects membership, then |s| = |t|.
Русский
Если существует биекция между s и t, сохраняющая принадлежности, то |s| = |t|.
LaTeX
$$∃Bijective between s and t ⇒ #s = #t$$
Lean4
/-- See also `card_bij`.
TODO: consider deprecating, since this has been unused in mathlib for a long time and is just a
special case of `card_bij`.
-/
theorem card_eq_of_bijective (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 = n := by
classical
have : s = (range n).attach.image fun i => f i.1 (mem_range.1 i.2) :=
by
ext a
suffices _ : a ∈ s ↔ ∃ (i : _) (hi : i ∈ range n), f i (mem_range.1 hi) = a by
simpa only [mem_image, mem_attach, true_and, Subtype.exists]
constructor
· intro ha; obtain ⟨i, hi, rfl⟩ := hf a ha; use i, mem_range.2 hi
· rintro ⟨i, hi, rfl⟩; apply hf'
calc
#s = #((range n).attach.image fun i => f i.1 (mem_range.1 i.2)) := by rw [this]
_ = #(range n).attach := ?_
_ = #(range n) := card_attach
_ = n := card_range n
apply card_image_of_injective
intro ⟨i, hi⟩ ⟨j, hj⟩ eq
exact Subtype.eq <| f_inj i j (mem_range.1 hi) (mem_range.1 hj) eq
