ssubset_iff

Mathlib.Data.Finset.Insert

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

English

A strict subset relation s ⊂ t is equivalent to the existence of a ∉ s with insert a s ⊆ t.

Русский

Строгое подмножество s ⊂ t эквивалентно существованию a ∉ s такого, что insert a s ⊆ t.

LaTeX

$$$s \\subset t \\iff \\exists a \\notin s, \\operatorname{insert}(a,s) \\subseteq t$$$

Lean4

theorem ssubset_iff : s ⊂ t ↔ ∃ a ∉ s, insert a s ⊆ t :=
  mod_cast @Set.ssubset_iff_insert α s t

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

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

Разделы

Аффилиация

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