apply_mono

Mathlib.Order.OmegaCompletePartialOrder

URI: https://scilib.ai/kg/mathlib#OmegaCompletePartialOrder.ContinuousHom.apply_mono

English

Continuity in the language of ωScottContinuous: F(ωSup C) = ωSup (C.map F).

Русский

Непрерывность в терминах ωScottContinuous: F(ωSup C) = ωSup(C.map F).

LaTeX

$$$F(\omegaSup C) = \omegaSup(C.map F)$$$

Lean4

@[mono]
theorem apply_mono {f g : α →𝒄 β} {x y : α} (h₁ : f ≤ g) (h₂ : x ≤ y) : f x ≤ g y :=
  OrderHom.apply_mono (show (f : α →o β) ≤ g from h₁) h₂

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

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

Разделы

Аффилиация

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