adj_incidenceSet_inter — Mathlib

English

If e ∈ E and v ∈ e, then the incidence of v intersects the incidence of the other endpoint in exactly e.

Русский

Если e ∈ E и v ∈ e, то пересечение инцидентностей v и другой вершины в точности равно e.

LaTeX

$$Let e ∈ G.edgeSet and v ∈ e; denote u as the other endpoint of e. Then G.incidenceSet(v) ∩ G.incidenceSet(u) = \\{ e \\}.$$

Lean4

theorem adj_incidenceSet_inter {v : V} {e : Sym2 V} (he : e ∈ G.edgeSet) (h : v ∈ e) :
    G.incidenceSet v ∩ G.incidenceSet (Sym2.Mem.other h) = { e } :=
  by
  ext e'
  simp only [incidenceSet, Set.mem_sep_iff, Set.mem_inter_iff, Set.mem_singleton_iff]
  refine ⟨fun h' => ?_, ?_⟩
  · rw [← Sym2.other_spec h]
    exact (Sym2.mem_and_mem_iff (edge_other_ne G he h).symm).mp ⟨h'.1.2, h'.2.2⟩
  · rintro rfl
    exact ⟨⟨he, h⟩, he, Sym2.other_mem _⟩

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