ssubset_iff_sdiff_singleton

Mathlib.Order.BooleanAlgebra.Set

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

English

If s ⊆ t, then t \\ (t \\ s) = s.

Русский

Если S ⊆ T, то T \\\\ (T \\\\ S) = S.

LaTeX

$$$ s \\subseteq t \\Rightarrow t \\\\setminus (t \\\\setminus s) = s $$$

Lean4

theorem ssubset_iff_sdiff_singleton : s ⊂ t ↔ ∃ a ∈ t, s ⊆ t \ { a } := by
  simp [ssubset_iff_insert, subset_diff, insert_subset_iff]; aesop

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

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

Разделы

Аффилиация

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