directed — Mathlib

English

A chain c is directed with respect to ≤, i.e., any two elements in the range of c have an upper bound in the range of c.

Русский

Цепь c направлена относительно порядка ≤; для любых двух элементов из диапазона c существует верхняя граница внутри диапазона c.

LaTeX

$$Directed (≤) c$$

Lean4

theorem directed : Directed (· ≤ ·) c :=
  directedOn_range.2 c.isChain_range.directedOn

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