English
Equivalent types V and W yield equivalent simple graphs; there is a natural equivalence between SimpleGraph V and SimpleGraph W induced by any equivalence e: V ≃ W.
Русский
Эквивалентные множества V и W порождают эквивалентные простые графы; между SimpleGraph V и SimpleGraph W существует естественная эквивалентность, индуцированная эквивалентностью e: V ≃ W.
LaTeX
$$$ \\text{Equiv.simpleGraph}(e) : \\mathrm{SimpleGraph}(V) \\simeq \\mathrm{SimpleGraph}(W) $$$
Lean4
/-- Equivalent types have equivalent simple graphs. -/
@[simps apply]
protected def _root_.Equiv.simpleGraph (e : V ≃ W) : SimpleGraph V ≃ SimpleGraph W
where
toFun := SimpleGraph.comap e.symm
invFun := SimpleGraph.comap e
left_inv _ := by simp
right_inv _ := by simp
