English
There is a natural equivalence between Fin n and graph f given by i ↦ (f(i), i).
Русский
Существует естественное эквиваленто между Fin n и graph f, задаваемое i ↦ (f(i), i).
LaTeX
$$$\\mathrm{graphEquiv}_1(f) : \\mathrm{Fin}\,n \\simeq \\mathrm{graph}(f)\\text{ via } i \\mapsto ((f(i), i),\\text{proof}).$$$
Lean4
/-- `graphEquiv₁ f` is the natural equivalence between `Fin n` and `graph f`,
mapping `i` to `(f i, i)`. -/
def graphEquiv₁ (f : Fin n → α) : Fin n ≃ graph f
where
toFun i := ⟨(f i, i), by simp [graph]⟩
invFun p := p.1.2
left_inv i := by simp
right_inv := fun ⟨⟨x, i⟩, h⟩ => by
-- Porting note: was `simpa [graph] using h`
simp only [graph, Finset.mem_image, Finset.mem_univ, true_and] at h
obtain ⟨i', hi'⟩ := h
obtain ⟨-, rfl⟩ := Prod.mk_inj.mp hi'
simpa
