notMem_of_notMem_sUnion

Mathlib.Data.Set.Lattice

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

English

If x is not in the union of S, and t ∈ S, then x is not in t.

Русский

Если x не принадлежит объединению ⋃S, и t ∈ S, то x не принадлежит t.

LaTeX

$$$ x \notin \bigcup S \rightarrow t \in S \rightarrow x \notin t $$$

Lean4

theorem notMem_of_notMem_sUnion {x : α} {t : Set α} {S : Set (Set α)} (hx : x ∉ ⋃₀ S) (ht : t ∈ S) : x ∉ t := fun h =>
  hx ⟨t, ht, h⟩

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

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

Разделы

Аффилиация

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