to_isDirected_le — Mathlib

English

In an order with a top element, any two elements have an upper bound (namely the top).

Русский

В порядке с верхней границей любой пары элементов имеет верхнюю границу (равную максимуму).

LaTeX

$$$\forall a,b \in \alpha, \ a \le \top \land b \le \top.$$$

Lean4

instance (priority := 100) to_isDirected_le [LE α] [OrderTop α] : IsDirected α (· ≤ ·) :=
  ⟨fun _ _ => ⟨⊤, le_top _, le_top _⟩⟩
    -- see Note [lower instance priority]

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