directed_le — Mathlib

English

If f is monotone and α is directed under ≤, β is a preorder, then f is directed with respect to ≤.

Русский

Если f монотонна и α направлено относительно ≤, а β является частичным порядком, то f направлена по отношению ≤.

LaTeX

$$$\text{Monotone}(f) \rightarrow Directed(\le, f)$$$

Lean4

theorem directed_le [Preorder α] [IsDirected α (· ≤ ·)] [Preorder β] {f : α → β} : Monotone f → Directed (· ≤ ·) f :=
  directed_of_isDirected_le

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