coe_iInf — Mathlib

English

For any index set ι and a family f: ι → G.Finsubgraph, the infimum of the family in finsubgraph terms equals the infimum of the family viewed as subgraphs of G.

Русский

Для любого индекса ι и семейства f: ι → G.Finsubgraph, нижняя граница семейства в рамках finsubgraph равна нижней границе, рассматриваемой как подграфы G.

LaTeX

$$$$ \\big\\langle i, f(i) \\big\\rangle_{i} = \\Bigl( \\big\\langle i, f(i) \\Bigr\\rangle_{i} : G.Subgraph \\Bigr). $$$$

Lean4

@[simp, norm_cast]
theorem coe_iInf {ι : Sort*} (f : ι → G.Finsubgraph) : ⨅ i, f i = (⨅ i, f i : G.Subgraph) := by
  rw [iInf, coe_sInf, iInf_range]

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