English
If there exists a bijection between s and t realized via a map i with maps to and from, then |s| = |t|.
Русский
Если существует биекция между s и t, реализованная через отображение i с отображениями в обе стороны, то |s| = |t|.
LaTeX
$$card_nbij ...$$
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_nbij'` is that the bijection is specified as a surjective
injection, rather than by an inverse function.
The difference with `Finset.card_bij` is that the bijection is a non-dependent function, rather than
being allowed to use membership of the domain. -/
theorem card_nbij (i : α → β) (hi : Set.MapsTo i s t) (i_inj : (s : Set α).InjOn i) (i_surj : (s : Set α).SurjOn i t) :
#s = #t :=
card_bij (fun a _ ↦ i a) hi i_inj (by simpa using i_surj)
