isAcyclic_iff — Mathlib

English

Isomorphic graphs are acyclic together: G IsAcyclic iff G' IsAcyclic under a graph isomorphism.

Русский

Изоморфные графы ациклически связаны: граф G ацикличен тогда и только тогда, когда граф G' также ацикличен под изоморфизмом.

LaTeX

$$$\\forall f : G \\cong_g G', \\; G.IsAcyclic \\iff G'.IsAcyclic$$$

Lean4

/-- Isomorphic graphs are acyclic together. -/
theorem isAcyclic_iff (f : G ≃g G') : G.IsAcyclic ↔ G'.IsAcyclic :=
  ⟨fun h ↦ h.embedding f.symm, fun h ↦ h.embedding f⟩

Похожие утверждения