incidenceSet_inter_incidenceSet_subset

English

If a ≠ b, then the intersection of edges incident to a and b is contained in the single edge {a,b}.

Русский

Пусть a ≠ b. Пересечение множеств ребер, инцидентных одновременно a и b, содержится в единственном ребре {a,b}.

LaTeX

$$$a \\neq b \\Rightarrow G.incidenceSet(a) \\cap G.incidenceSet(b) \\subseteq \\{ s(a,b) \\}$$$

Lean4

theorem incidenceSet_inter_incidenceSet_subset (h : a ≠ b) : G.incidenceSet a ∩ G.incidenceSet b ⊆ {s(a, b)} :=
  fun _e he => (Sym2.mem_and_mem_iff h).1 ⟨he.1.2, he.2.2⟩

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