verts_iInf — Mathlib

English

The vertex set of the infimum over an index is the intersection of vertex sets of the indexed subgraphs.

Русский

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

LaTeX

$$$ (\\\\iInf i, f i).verts = \\\\bigcap i, (f i).verts $$$

Lean4

@[simp]
theorem verts_iInf {f : ι → G.Subgraph} : (⨅ i, f i).verts = ⋂ i, (f i).verts := by simp [iInf]

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