edgeSet_sSup — Mathlib

English

For a set S of subgraphs of G, the edge set of the supremum is the union over all, i.e., (sSup S).edgeSet = ⋃_{G' ∈ S} edgeSet(G').

Русский

Для множества S подграфов G верхний предел имеет множество рёбер, равное объединению множеств рёбер всех элементов: (sSup S).edgeSet = ⋃_{G' ∈ S} edgeSet(G').

LaTeX

$$$ (sSup S).edgeSet = \bigcup_{G' \in S} edgeSet(G') $$$

Lean4

@[simp]
theorem edgeSet_sSup (s : Set G.Subgraph) : (sSup s).edgeSet = ⋃ G' ∈ s, edgeSet G' :=
  by
  ext e
  induction e
  simp

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