diff_subset

Mathlib.Order.BooleanAlgebra.Set

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

English

For all sets s,t, s \ t ⊆ s.

Русский

Для любых множеств s,t верно: s \ t ⊆ s.

LaTeX

$$$s \setminus t \subseteq s$$$

Lean4

theorem diff_subset {s t : Set α} : s \ t ⊆ s :=
  show s \ t ≤ s from sdiff_le

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

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

Разделы

Аффилиация

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