edgeSet_iInf — Mathlib

English

For a family f: ι → G.Subgraph, the edge set of the infimum equals the intersection over i of edgeSets, then intersected with G.edgeSet: (iInf f).edgeSet = (⋂ i, (f i).edgeSet) ∩ G.edgeSet.

Русский

Для семейства f: ι → G.Subgraph множество рёбер инфимума равно пересечению по i множеств рёбер, затем пересечению с edgeSet G: (iInf f).edgeSet = (⋂ i, (f i).edgeSet) ∩ G.edgeSet.

LaTeX

$$$ (\\mathrm{iInf} \\ f).edgeSet = (\\bigcap i, (f(i)).edgeSet) \\cap G.edgeSet $$$

Lean4

@[simp]
theorem edgeSet_iInf (f : ι → G.Subgraph) : (⨅ i, f i).edgeSet = (⋂ i, (f i).edgeSet) ∩ G.edgeSet := by simp [iInf]

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