div_right

Mathlib.Algebra.Order.UpperLower

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

English

If S is a lower set, then the right-division S / T is also a lower set for any T.

Русский

Если S — нижнее множество, то S / T также является нижним множеством для любого T.

LaTeX

$$$\\text{IsLowerSet}(S) \\Rightarrow \\text{IsLowerSet}(S / T)$$$

Lean4

@[to_additive]
theorem div_right (hs : IsLowerSet s) : IsLowerSet (s / t) :=
  hs.toDual.div_right

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

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

Разделы

Аффилиация

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