English
For finite α, β and a function f: α → β, f is bijective iff map f univ α = univ β.
Русский
Для конечных типов α, β и функции f: α → β, f является биективной тогда и только тогда, когда map f univ α = univ β.
LaTeX
$$$$ f \\text{ Bijective } \\iff \\operatorname{map} f (\\operatorname{univ} : \\mathrm{Finset} \\; \\alpha).\\mathrm{val} = \\operatorname{univ}.\\mathrm{val}. $$$$
Lean4
/-- For functions on finite sets, they are bijections iff they map universes into universes. -/
@[simp]
theorem bijective_iff_map_univ_eq_univ (f : α → β) : f.Bijective ↔ map f (Finset.univ : Finset α).val = univ.val :=
⟨fun bij ↦ congr_arg (·.val) (map_univ_equiv <| Equiv.ofBijective f bij), fun eq ↦
⟨fun a₁ a₂ ↦ inj_on_of_nodup_map (eq.symm ▸ univ.nodup) _ (mem_univ a₁) _ (mem_univ a₂), fun b ↦
have ⟨a, _, h⟩ := mem_map.mp (eq.symm ▸ mem_univ_val b);
⟨a, h⟩⟩⟩
