coe_iSup — Mathlib

English

For any index set ι and a family f: ι → G.Finsubgraph, the supremum of the family in the finsubgraph sense coincides with the supremum of the same family viewed as subgraphs of G.

Русский

Для любого индекcного набора ι и семейства f: ι → G.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_iSup {ι : Sort*} (f : ι → G.Finsubgraph) : ⨆ i, f i = (⨆ i, f i : G.Subgraph) := by
  rw [iSup, coe_sSup, iSup_range]

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