directed_ge

Mathlib.Order.Directed

URI: https://scilib.ai/kg/mathlib#Antitone.directed_ge

← MathLib Explorer

English

If f is antitone, then directed with respect to ≥.

Русский

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

LaTeX

$$$\text{Antitone}(f) \rightarrow Directed(\ge, f)$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru