isTree_iff — Mathlib

English

If two graphs are isomorphic, then being a tree is preserved: G is a tree iff G' is a tree.

Русский

Если два графа изоморфны, то свойство быть деревом сохраняется: G является деревом тогда и только тогда, когда G' является деревом.

LaTeX

$$$\forall f: G \cong G',\ G.IsTree \iff G'.IsTree$$$

Lean4

/-- Isomorphic graphs are trees together. -/
theorem isTree_iff (f : G ≃g G') : G.IsTree ↔ G'.IsTree :=
  ⟨fun ⟨hc, ha⟩ ↦ ⟨f.connected_iff.mp hc, f.isAcyclic_iff.mp ha⟩, fun ⟨hc, ha⟩ ↦
    ⟨f.connected_iff.mpr hc, f.isAcyclic_iff.mpr ha⟩⟩

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