ssubset_of_mem_notMem

Mathlib.Data.Set.Insert

URI: https://scilib.ai/kg/mathlib#HasSubset.Subset.ssubset_of_mem_notMem

English

If s ⊆ t and a ∈ t and a ∉ s, then s ⊊ t.

Русский

Если s ⊆ t и существует a ∈ t, но a ∉ s, тогда s ⊊ t.

LaTeX

$$$$ (s \\subseteq t) \\land (a \\in t) \\land (a \\notin s) \\Rightarrow s \\subset t $$$$

Lean4

theorem _root_.HasSubset.Subset.ssubset_of_mem_notMem (hst : s ⊆ t) (hat : a ∈ t) (has : a ∉ s) : s ⊂ t := by grind

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

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

Разделы

Аффилиация

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