English
A variant of card_bij where the bijection is given with an inverse function.
Русский
Вариант card_bij, где биекция задается через обратную функцию.
LaTeX
$$card_bij' ...$$
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 with an inverse, rather
than as a surjective injection.
The difference with `Finset.card_nbij'` is that the bijection and its inverse are allowed to use
membership of the domains, rather than being non-dependent functions. -/
theorem card_bij' (i : ∀ a ∈ s, β) (j : ∀ a ∈ t, α) (hi : ∀ a ha, i a ha ∈ t) (hj : ∀ a ha, j a ha ∈ s)
(left_inv : ∀ a ha, j (i a ha) (hi a ha) = a) (right_inv : ∀ a ha, i (j a ha) (hj a ha) = a) : #s = #t :=
by
refine card_bij i hi (fun a1 h1 a2 h2 eq ↦ ?_) (fun b hb ↦ ⟨_, hj b hb, right_inv b hb⟩)
rw [← left_inv a1 h1, ← left_inv a2 h2]
simp only [eq]
