notMem_compl

Mathlib.Data.Finset.BooleanAlgebra

URI: https://scilib.ai/kg/mathlib#Finset.notMem_compl

English

Not membership in the complement is equivalent to membership in the original set: a ∉ s^c ↔ a ∈ s.

Русский

Не-членство в дополнении эквивалентно членству в множестве: a ∉ s^c ↔ a ∈ s.

LaTeX

$$$a \notin s^{c} \iff a \in s$$$

Lean4

theorem notMem_compl : a ∉ sᶜ ↔ a ∈ s := by rw [mem_compl, not_not]

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

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

Разделы

Аффилиация

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