sdiff_of_isUpperSet

Mathlib.Order.UpperLower.Basic

URI: https://scilib.ai/kg/mathlib#IsLowerSet.sdiff_of_isUpperSet

English

If s is lower and t is upper, then s \\ t is lower.

Русский

Если s — нижнее множество, а t — верхнее, то s \\ t — нижнее.

LaTeX

$$$IsLowerSet s \\to IsUpperSet t \\to IsLowerSet (s \\ t)$$$

Lean4

theorem sdiff_of_isUpperSet (hs : IsLowerSet s) (ht : IsUpperSet t) : IsLowerSet (s \ t) :=
  hs.sdiff <| by aesop

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

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

Разделы

Аффилиация

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