English
The two sets (edgeFinset \ incidenceFinset t) and image(neighborFinset s) under s(·,t) are disjoint.
Русский
Два множества (edgeFinset \ incidenceFinset t) и image(neighborFinset s) под отображением s(·,t) попарно непересекаются.
LaTeX
$$$ \operatorname{Disjoint} \big( G.edgeFinset \ G.incidenceFinset t \big) \big( \operatorname{image}(x \mapsto \operatorname{Sym2.mk}\{ fst := x, snd := t \})( G.neighborFinset s ) \big) $$$
Lean4
theorem disjoint_sdiff_neighborFinset_image :
Disjoint (G.edgeFinset \ G.incidenceFinset t) ((G.neighborFinset s).image (s(·, t))) :=
by
rw [disjoint_iff_ne]
intro e he
have : t ∉ e := by
rw [mem_sdiff, mem_incidenceFinset] at he
obtain ⟨_, h⟩ := he
contrapose! h
simp_all [incidenceSet]
aesop