spanningCoe_inj — Mathlib

English

Equality of spanningCoe implies equality of adjacency in the subgraphs: G₁.spanningCoe = G₂.spanningCoe if and only if G₁.Adj = G₂.Adj.

Русский

Равенство spanningCoe в подграфах эквивалентно равенству их смежности: G₁.spanningCoe = G₂.spanningCoe ⇔ G₁.Adj = G₂.Adj.

LaTeX

$$G₁.spanningCoe = G₂.spanningCoe ↔ G₁.Adj = G₂.Adj$$

Lean4

theorem spanningCoe_inj : G₁.spanningCoe = G₂.spanningCoe ↔ G₁.Adj = G₂.Adj := by simp [Subgraph.spanningCoe]

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