insert_diff_of_mem

Mathlib.Order.BooleanAlgebra.Set

URI: https://scilib.ai/kg/mathlib#Set.insert_diff_of_mem

English

Disjoint (s \\\\setminus t) and (s ∩ t).

Русский

Разность, пересечение — несовместны.

LaTeX

$$$ (s \\\\setminus t) \\\\cap (s \\\\cap t) = \\\\emptyset $$$

Lean4

@[simp]
theorem insert_diff_of_mem (s) (h : a ∈ t) : insert a s \ t = s \ t := by grind

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru