directed_of_isDirected_le — Mathlib

English

Let α be directed under ≤ and f: α → β. If i ≤ j implies r(f(i), f(j)) for all i,j, then f is directed w.r.t. r.

Русский

Пусть α направлено относительно ≤ и есть функция f: α → β. Если для всех i ≤ j выполняется r(f(i), f(j)), то f направлена по отношению r.

LaTeX

$$$IsDirected(\alpha, \le) \rightarrow (\forall i,j,\ i \le j \rightarrow r(f(i),f(j))) \rightarrow Directed(r,f)$$$

Lean4

/-- A monotone function on an upwards-directed type is directed. -/
theorem directed_of_isDirected_le [LE α] [IsDirected α (· ≤ ·)] {f : α → β} {r : β → β → Prop}
    (H : ∀ ⦃i j⦄, i ≤ j → r (f i) (f j)) : Directed r f :=
  directed_id.mono_comp _ H

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