diff_insert_of_notMem

Mathlib.Order.BooleanAlgebra.Set

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

English

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

Русский

Несовместность множества s и (t \\ s).

LaTeX

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

Lean4

theorem diff_insert_of_notMem (h : a ∉ s) : s \ insert a t = s \ t := by grind

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

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

Разделы

Аффилиация

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