isRelLowerSet

Mathlib.Order.UpperLower.Relative

URI: https://scilib.ai/kg/mathlib#RelLowerSet.isRelLowerSet

English

Any RelLowerSet P induces that its underlying set is an IsRelLowerSet with respect to P.

Русский

Любое RelLowerSet P порождает то, что лежащее под ним множество является IsRelLowerSet относительно P.

LaTeX

$$$IsRelLowerSet (\mathrm{underlying}(l)) P$$$

Lean4

theorem isRelLowerSet (l : RelLowerSet P) : IsRelLowerSet l P :=
  l.isRelLowerSet'

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

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

Разделы

Аффилиация

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