verts_iSup — Mathlib

English

The vertex set of the supremum over an index is the union of the vertex sets of the indexed subgraphs.

Русский

Множество вершин наибольшего по индексу подграфа — это объединение вершин всех подграфов с индексами.

LaTeX

$$$ (\\\\iSup i, f i).verts = \\\\bigcup i, (f i).verts $$$

Lean4

@[simp]
theorem verts_iSup {f : ι → G.Subgraph} : (⨆ i, f i).verts = ⋃ i, (f i).verts := by simp [iSup]

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