edgeSet_iSup — Mathlib

English

For a family f: ι → G.Subgraph, the edge set of the supremum equals the union over indices: (iSup i, f i).edgeSet = ⋃ i, (f i).edgeSet.

Русский

Для семейства f: ι → G.Subgraph множество рёбер верхнего предела равно объединению по индексам: (iSup i, f i).edgeSet = ⋃ i, (f i).edgeSet.

LaTeX

$$$ (\\mathrm{iSup} \ f).edgeSet = \\bigcup_i (f(i)).edgeSet $$$

Lean4

@[simp]
theorem edgeSet_iSup (f : ι → G.Subgraph) : (⨆ i, f i).edgeSet = ⋃ i, (f i).edgeSet := by simp [iSup]

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