mem_compl

Mathlib.ModelTheory.Definability

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.DefinableSet.mem_compl

English

Membership in the complement is the negation of membership.

Русский

Принадлежность к комплементу есть отрицание принадлежности.

LaTeX

$$$$ x \\in s^c \\iff x \\notin s. $$$$

Lean4

@[simp]
theorem mem_compl : x ∈ sᶜ ↔ x ∉ s :=
  Iff.rfl

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

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

Разделы

Аффилиация

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