English
A more general bijection with inverse properties ensuring equal cardinalities.
Русский
Более общая биекция с обратной связью для равенства кардиналов.
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 with an inverse, rather
than as a surjective injection.
The difference with `Finset.card_bij'` is that the bijection and its inverse are non-dependent
functions, rather than being allowed to use membership of the domains.
The difference with `Finset.card_equiv` is that bijectivity is only required to hold on the domains,
rather than on the entire types. -/
theorem card_nbij' (i : α → β) (j : β → α) (hi : Set.MapsTo i s t) (hj : Set.MapsTo j t s)
(left_inv : Set.LeftInvOn j i s) (right_inv : Set.RightInvOn j i t) : #s = #t :=
card_bij' (fun a _ ↦ i a) (fun b _ ↦ j b) hi hj left_inv right_inv
