isSpanning — Mathlib

English

The subgraph obtained by restricting H to G is spanning in G: IsSpanning(toSubgraph(H,h)).

Русский

Подграф, получаемый ограничением H к G, является полноцветным (покрывающим все вершины) в G: IsSpanning(toSubgraph(H,h)).

LaTeX

$$$ IsSpanning\left(\text{toSubgraph}(H,h)\right) $$$

Lean4

theorem _root_.SimpleGraph.toSubgraph.isSpanning (H : SimpleGraph V) (h : H ≤ G) : (toSubgraph H h).IsSpanning :=
  Set.mem_univ

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