to_isDirected_ge — Mathlib

English

A semilattice_inf is directed under the reversed order via infimum.

Русский

Полуупорядоченное по inf образует направленность при порядке ≥ через знак наименьшего общего предка.

LaTeX

$$$\forall \alpha, [SemilatticeInf \alpha], IsDirected \alpha (GE.ge).$$$

Lean4

instance (priority := 100) to_isDirected_ge [SemilatticeInf α] : IsDirected α (· ≥ ·) :=
  ⟨fun a b => ⟨a ⊓ b, inf_le_left, inf_le_right⟩⟩
    -- see Note [lower instance priority]

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