edgeSet_sdiff_sdiff_isDiag — Mathlib

English

G.edgeSet \ (s \ {e | e.IsDiag}) = G.edgeSet \ s for any G and s.

Русский

G.edgeSet \ (s \ {e | e.IsDiag}) = G.edgeSet \ s для любых G и s.

LaTeX

$$$$ G.edgeSet \ (s \ {e \mid e.IsDiag}) = G.edgeSet \ s. $$$$

Lean4

/-- This lemma, combined with `edgeSet_sdiff` and `edgeSet_from_edgeSet`,
allows proving `(G \ from_edgeSet s).edge_set = G.edgeSet \ s` by `simp`. -/
@[simp]
theorem edgeSet_sdiff_sdiff_isDiag (G : SimpleGraph V) (s : Set (Sym2 V)) :
    G.edgeSet \ (s \ {e | e.IsDiag}) = G.edgeSet \ s := by
  ext e
  simp only [Set.mem_diff, Set.mem_setOf_eq, not_and, not_not, and_congr_right_iff]
  intro h
  simp only [G.not_isDiag_of_mem_edgeSet h, imp_false]

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