comp_le_comp_left

Mathlib.Order.Monotone.Defs

URI: https://scilib.ai/kg/mathlib#Monotone.comp_le_comp_left

← MathLib Explorer

English

If f is monotone and g ≤ h, then f ∘ g ≤ f ∘ h as functions.

Русский

Если f монотонна и g ≤ h, то f ∘ g ≤ f ∘ h (почему точечно).

LaTeX

$$$\\mathrm{Monotone}(f)\\to g\\le h\\to f\\circ g \\le f\\circ h$$$

Lean4

theorem comp_le_comp_left [Preorder β] {f : β → α} {g h : γ → β} (hf : Monotone f) (le_gh : g ≤ h) :
    LE.le.{max w u} (f ∘ g) (f ∘ h) := fun x ↦ hf (le_gh x)

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

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

Разделы

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

Аффилиация

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