le_iSup

Mathlib.Order.CompletePartialOrder

URI: https://scilib.ai/kg/mathlib#Directed.le_iSup

English

If f: ι → α is directed, then each f(i) ≤ ⨆ j, f(j).

Русский

Если f: ι → α направлено, то каждый f(i) ≤ ⨆_{j} f(j).

LaTeX

$$$\text{Directed}(\le)\ f \rightarrow \forall i,\ f(i) \le \bigvee_{j} f(j)$$$

Lean4

protected theorem le_iSup (hf : Directed (· ≤ ·) f) (i : ι) : f i ≤ ⨆ j, f j :=
  hf.directedOn_range.le_sSup <| Set.mem_range_self _

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

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

Разделы

Аффилиация

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