apply_mono

Mathlib.Order.Hom.Basic

URI: https://scilib.ai/kg/mathlib#OrderHom.apply_mono

English

If f ≤ g and x ≤ y then f x ≤ g y for OrderHom elements.

Русский

Если f ≤ g и x ≤ y, то f(x) ≤ g(y) для OrderHom.

LaTeX

$$$\\forall \\{f,g: α \\to_o β\\}\\;\\forall \\{x,y: α\\}\\; (h_1: f ≤ g) (h_2: x ≤ y),\\; f(x) ≤ g(y).$$$

Lean4

@[mono]
theorem apply_mono {f g : α →o β} {x y : α} (h₁ : f ≤ g) (h₂ : x ≤ y) : f x ≤ g y :=
  (h₁ x).trans <| g.mono h₂

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

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

Разделы

Аффилиация

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