notMem_union

Mathlib.Data.Finset.Lattice.Basic

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

English

An element is not in S ∪ T if and only if it is not in S and not in T.

Русский

Элемент не принадлежит S ∪ T тогда и только тогда, когда он не принадлежит S и не принадлежит T.

LaTeX

$$$ a \notin s \cup t \iff a \notin s \land a \notin t $$$

Lean4

theorem notMem_union : a ∉ s ∪ t ↔ a ∉ s ∧ a ∉ t := by rw [mem_union, not_or]

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

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

Разделы

Аффилиация

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