disjoint_sdiff_neighborFinset_image

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

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