sdiff_le_left

Mathlib.Order.UpperLower.Closure

URI: https://scilib.ai/kg/mathlib#LowerSet.sdiff_le_left

English

The sdiff is below s in the lattice order: s.sdiff t ≤ s.

Русский

Операция sdiff является подмножением к s в решетке: s.sdiff t ≤ s.

LaTeX

$$$ s.sdiff t \\le s $$$

Lean4

theorem sdiff_le_left : s.sdiff t ≤ s :=
  diff_subset

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

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

Разделы

Аффилиация

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