spanningCoeEquivCoeOfSpanning — Mathlib

English

For a subgraph G' of G that is IsSpanning, the spanningCoe (the embedding of the spanning subgraph) is isomorphic to the underlying coe graph: G'.spanningCoe ≃g G'.coe.

Русский

Для подграфа G' графа G, который является IsSpanning, отношение spanningCoe эквивалентно подграфу coe: существует изоморфизм G'.spanningCoe ≃g G'.coe.

LaTeX

$$$\forall (G' : G.Subgraph) (h : G'.IsSpanning),\; G'.spanningCoe \cong_g G'.coe.$$$

Lean4

/-- `spanningCoe` is equivalent to `coe` for a subgraph that `IsSpanning`. -/
@[simps]
def spanningCoeEquivCoeOfSpanning (G' : Subgraph G) (h : G'.IsSpanning) : G'.spanningCoe ≃g G'.coe
    where
  toFun v := ⟨v, h v⟩
  invFun v := v
  map_rel_iff' := Iff.rfl

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