incidenceSet_inter_incidenceSet_of_not_adj

English

If a ≠ b and a and b are not adjacent, then the incidence sets of a and b are disjoint.

Русский

Если a ≠ b и a не соседствует с b, то инцидентные множества a и b не пересекаются.

LaTeX

$$$\\neg G.Adj(a,b) \\land a \\neq b \\Rightarrow G.incidenceSet(a) \\cap G.incidenceSet(b) = \\emptyset$$$

Lean4

theorem incidenceSet_inter_incidenceSet_of_not_adj (h : ¬G.Adj a b) (hn : a ≠ b) :
    G.incidenceSet a ∩ G.incidenceSet b = ∅ :=
  by
  simp_rw [Set.eq_empty_iff_forall_notMem, Set.mem_inter_iff, not_and]
  intro u ha hb
  exact h (G.adj_of_mem_incidenceSet hn ha hb)

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