instIsDirectedLe — 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 such that a ≤ c и b ≤ c.

LaTeX

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

Lean4

instance (priority := 100) : IsDirected R (· ≤ ·) :=
  ⟨fun x y ↦
    let ⟨m, hm⟩ := exists_nat_ge x;
    let ⟨n, hn⟩ := exists_nat_ge y
    let ⟨k, hmk, hnk⟩ := exists_ge_ge m n
    ⟨k, hm.trans <| Nat.mono_cast hmk, hn.trans <| Nat.mono_cast hnk⟩⟩

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