sSup_le

Mathlib.Order.CompletePartialOrder

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

English

If d is directed and every element of d is ≤ a, then sSup d ≤ a.

Русский

Если d направлено и каждый элемент d ≤ a, тогда sSup d ≤ a.

LaTeX

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

Lean4

protected theorem sSup_le (hd : DirectedOn (· ≤ ·) d) (ha : ∀ b ∈ d, b ≤ a) : sSup d ≤ a :=
  hd.isLUB_sSup.2 ha

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

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

Разделы

Аффилиация

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