not_subset

Mathlib.Data.Set.Basic

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

English

Not s ⊆ t is equivalent to there exists an element of s not in t.

Русский

Неравенство подмножества: существует элемент множества s, которого нет в t.

LaTeX

$$$\\not\\subset \\Rightarrow \\exists a\\in s, a\\notin t$$$

Lean4

theorem not_subset : ¬s ⊆ t ↔ ∃ a ∈ s, a ∉ t := by simp only [subset_def, not_forall, exists_prop]

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

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

Разделы

Аффилиация

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