not_subset_iff_exists_mem_notMem

Mathlib.Data.Set.Basic

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

English

¬(s ⊆ t) ↔ ∃ x, x ∈ s ∧ x ∉ t

Русский

¬(s ⊆ t) эквивалентно ∃ x, x ∈ s и x ∉ t.

LaTeX

$$$\neg (s \subseteq t) \iff \exists x, x \in s \land x \notin t$$$

Lean4

theorem not_subset_iff_exists_mem_notMem {α : Type*} {s t : Set α} : ¬s ⊆ t ↔ ∃ x, x ∈ s ∧ x ∉ t := by simp [subset_def]

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

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

Разделы

Аффилиация

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