instMax — Mathlib

English

There is a natural notion of pointwise maximum on order-preserving maps: for f, g: α →o β, their maximum is given by (f ⊔ g)(a) = f(a) ⊔ g(a).

Русский

Существует естественное определение покоординатного максимума для отображений, сохраняющих порядок: для f, g: α →o β, максимум задаётся как (f ⊔ g)(a) = f(a) ⊔ g(a).

LaTeX

$$$\text{Max}.(f,g)\; :\; (f ⊔ g)(a) = f(a) ⊔ g(a).$$$

Lean4

instance [SemilatticeSup β] : Max (α →o β) where max f g := ⟨fun a => f a ⊔ g a, f.mono.sup g.mono⟩

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