not_subset

Mathlib.Data.Finset.Defs

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

English

Not (s ⊆ t) is equivalent to the existence of an element of s not in t.

Русский

Не s ⊆ t эквивалентно существованию элемента x ∈ s, которого нет в t.

LaTeX

$$$\forall s,t:\ Finset\ α,\ Iff (Not (s \subseteq t)) (Exists x \in s, x \notin t)$$$

Lean4

theorem not_subset : ¬s ⊆ t ↔ ∃ x ∈ s, x ∉ t := by simp only [← coe_subset, Set.not_subset, mem_coe]

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

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

Разделы

Аффилиация

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