incidenceSet_inter_incidenceSet_of_adj

English

If a is adjacent to b, then the intersection of their incidence sets is exactly {s(a,b)}.

Русский

Если a соседствует с b, то пересечение их инцидентных множеств равно ровно {s(a,b)}.

LaTeX

$$$G.Adj(a,b) \\Rightarrow G.incidenceSet(a) \\cap G.incidenceSet(b) = \\{ s(a,b) \\}$$$

Lean4

theorem incidenceSet_inter_incidenceSet_of_adj (h : G.Adj a b) : G.incidenceSet a ∩ G.incidenceSet b = {s(a, b)} :=
  by
  refine (G.incidenceSet_inter_incidenceSet_subset <| h.ne).antisymm ?_
  rintro _ (rfl : _ = s(a, b))
  exact ⟨G.mk'_mem_incidenceSet_left_iff.2 h, G.mk'_mem_incidenceSet_right_iff.2 h⟩

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