isRelUpperSet

Mathlib.Order.UpperLower.Relative

URI: https://scilib.ai/kg/mathlib#RelUpperSet.isRelUpperSet

English

Any RelUpperSet P induces that its underlying set is an IsRelUpperSet with respect to P.

Русский

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

LaTeX

$$$IsRelUpperSet (\mathrm{underlying}(u)) P$$$

Lean4

theorem isRelUpperSet (u : RelUpperSet P) : IsRelUpperSet u P :=
  u.isRelUpperSet'

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

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

Разделы

Аффилиация

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