ssubset_iff_insert

Mathlib.Data.Set.Insert

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

English

For sets s ⊂ t, there exists an a ∉ s such that insert a s ⊆ t.

Русский

Для множеств s ⊂ t существует a ∉ s, такое что insert a s ⊆ t.

LaTeX

$$$s \subset t \iff \exists a \notin s, insert a s \subseteq t$$$

Lean4

theorem ssubset_iff_insert {s t : Set α} : s ⊂ t ↔ ∃ a ∉ s, insert a s ⊆ t := by grind

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

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

Разделы

Аффилиация

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