le_sSup

Mathlib.Order.CompletePartialOrder

URI: https://scilib.ai/kg/mathlib#DirectedOn.le_sSup

English

If d is directed and a ∈ d, then a ≤ sSup d.

Русский

Если d направлено и a ∈ d, тогда a ≤ sSup d.

LaTeX

$$$\text{DirectedOn}(\le)\ d \rightarrow a \in d \rightarrow a \le sSup\ d$$$

Lean4

protected theorem le_sSup (hd : DirectedOn (· ≤ ·) d) (ha : a ∈ d) : a ≤ sSup d :=
  hd.isLUB_sSup.1 ha

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

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

Разделы

Аффилиация

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