isSpanning_iff — Mathlib

English

A subgraph G' is spanning if and only if its vertex set equals the entire vertex set of G.

Русский

Подграф G' является растяжимым (spanning) тогда и только тогда, когда множество вершин G' равно всему множеству вершин G.

LaTeX

$$G'.IsSpanning ⇔ G'.verts = Set.univ$$

Lean4

theorem isSpanning_iff {G' : Subgraph G} : G'.IsSpanning ↔ G'.verts = Set.univ :=
  Set.eq_univ_iff_forall.symm

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