deleteEdges_inter_edgeSet_right_eq

English

Deleting edges on the intersection with edgeSet is the same as deleting on the whole set (symmetric statement).

Русский

Удаление рёбер на пересечении с edgeSet эквивалентно удалению на всём множестве.

LaTeX

$$$ G'.deleteEdges( s \\cap G'.edgeSet ) = G'.deleteEdges(s) $$$

Lean4

@[simp]
theorem deleteEdges_inter_edgeSet_right_eq : G'.deleteEdges (s ∩ G'.edgeSet) = G'.deleteEdges s := by
  ext <;> simp +contextual [imp_false]

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