English
If there exists a bijection between s and t implemented via a dependent constructor, then |s| = |t|.
Русский
Если существует биекция между s и t, реализованная через зависимую конструктор, то |s| = |t|.
LaTeX
$$∀ i, ∀ hi, ∀ ... ⇒ #s = #t$$
Lean4
/-- Given a bijection from a finite set `s` to a finite set `t`, the cardinalities of `s` and `t`
are equal.
The difference with `Finset.card_bij'` is that the bijection is specified as a surjective injection,
rather than by an inverse function.
The difference with `Finset.card_nbij` is that the bijection is allowed to use membership of the
domain, rather than being a non-dependent function. -/
theorem card_bij (i : ∀ a ∈ s, β) (hi : ∀ a ha, i a ha ∈ t) (i_inj : ∀ a₁ ha₁ a₂ ha₂, i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂)
(i_surj : ∀ b ∈ t, ∃ a ha, i a ha = b) : #s = #t := by
classical
calc
#s = #s.attach := card_attach.symm
_ = #(s.attach.image fun a ↦ i a.1 a.2) := (Eq.symm ?_)
_ = #t := ?_
· apply card_image_of_injective
intro ⟨_, _⟩ ⟨_, _⟩ h
simpa using i_inj _ _ _ _ h
· congr 1
ext b
constructor <;> intro h
· obtain ⟨_, _, rfl⟩ := mem_image.1 h; apply hi
· obtain ⟨a, ha, rfl⟩ := i_surj b h; exact mem_image.2 ⟨⟨a, ha⟩, by simp⟩
