sdiff_sep_self

Mathlib.Order.BooleanAlgebra.Set

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

English

For any set S and predicate P on elements, S \\ { x ∈ S | P(x) } = { x ∈ S | ¬ P(x) }.

Русский

Для множества S и предиката P верно: S \\ { x ∈ S | P(x) } = { x ∈ S | ¬ P(x) }.

LaTeX

$$$ s \\\\setminus \\{ x \\\\in s \\\\mid p(x) \\\\} = \\{ x \\\\in s \\\\mid \\neg p(x) \\\\} $$$

Lean4

@[simp]
theorem sdiff_sep_self (s : Set α) (p : α → Prop) : s \ {a ∈ s | p a} = {a ∈ s | ¬p a} :=
  diff_self_inter

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

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

Разделы

Аффилиация

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