coe_sSup — Mathlib

English

Let V be finite and G a simple graph on V. For any set s of finite subgraphs of G, the supremum of s in the lattice of subgraphs is obtained by taking the join of all members of s when viewed as subgraphs of G.

Русский

Пусть V конечен, и G — простой граф на V. Для любой множества s конечных подграфов G находимый предел (супремум) множества s в решёшении подграфов достигается объединением всех элементов s, рассматриваемых как подграфы G.

LaTeX

$$$$ \\operatorname{sSup}(s) = \\bigvee_{G' \\in s} \\bigl(G' : G'.\\mathrm{Subgraph}\\bigr). $$$$

Lean4

@[simp, norm_cast]
theorem coe_sSup (s : Set G.Finsubgraph) : sSup s = (⨆ G ∈ s, G : G.Subgraph) :=
  rfl

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