edgeSet_inf — Mathlib

English

For subgraphs H1, H2 of G, the edge set of their infimum equals the intersection: (H1 ⊓ H2).edgeSet = H1.edgeSet ∩ H2.edgeSet.

Русский

Для подграфов H1, H2 графа G множество рёбер их инфимума равно пересечению соответствующих множеств рёбер: (H1 ⊓ H2).edgeSet = H1.edgeSet ∩ H2.edgeSet.

LaTeX

$$$ (H_1 \\sqcap H_2).edgeSet = H_1.edgeSet \\cap H_2.edgeSet $$$

Lean4

@[simp]
theorem edgeSet_inf {H₁ H₂ : Subgraph G} : (H₁ ⊓ H₂).edgeSet = H₁.edgeSet ∩ H₂.edgeSet :=
  Set.ext <| Sym2.ind (by simp)

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