instIsDirectedGe — Mathlib

English

The ≥ relation on an Archimedean ring is directed: for any a,b there exists c with a ≥ c and b ≥ c.

Русский

Отношение ≥ на Архимедовом кольце направлено: для любых a,b существует c такой, что a ≥ c и b ≥ c.

LaTeX

$$$\\forall a,b,\\ exists\\ c:\\, R\\,(a \\ge c \\land b \\ge c).$$$

Lean4

instance (priority := 100) : IsDirected R (· ≥ ·) where
  directed a
    b :=
    let ⟨m, hm⟩ := exists_int_le a;
    let ⟨n, hn⟩ := exists_int_le b
    ⟨(min m n : ℤ), le_trans (Int.cast_mono <| min_le_left _ _) hm, le_trans (Int.cast_mono <| min_le_right _ _) hn⟩

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