directed_ge — Mathlib

English

If α is directed under ≥ and f is monotone, then f is directed with respect to ≥.

Русский

Если α направлено по ≥ и функция f монотонна, то f направлена по ≥.

LaTeX

$$$IsDirected(\alpha, \ge) \rightarrow (Monotone(f)) \rightarrow Directed(\ge, f)$$$

Lean4

theorem directed_ge [Preorder α] [IsDirected α (· ≥ ·)] [Preorder β] {f : α → β} (hf : Monotone f) :
    Directed (· ≥ ·) f :=
  directed_of_isDirected_ge hf

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