directed_le — Mathlib

English

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

Русский

Если f антитонна и α направлено по ≥, тогда f направлена по ≤.

LaTeX

$$$IsDirected(\alpha, \ge) \rightarrow (Antitone(f)) \rightarrow Directed(\le, f)$$$

Lean4

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

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