instSup — Mathlib

English

The supremum (maximum) of two μ-ae equivalence classes is defined pointwise via the supremum operation on β, yielding a new μ-ae equivalence class.

Русский

Наибольший элемент двух μ-аe эквивалентных классов задается покомпонентно через операцию на β, образуя новый класс.

LaTeX

$$$\text{Max}(\alpha \to_μ β)$ with $(f ⊔ g)$ defined by $(f ⊔ g)(a) = f(a) \;\uparrow\; g(a)$ a.e.$$

Lean4

instance instSup : Max (α →ₘ[μ] β) where max f g := AEEqFun.comp₂ (· ⊔ ·) continuous_sup f g

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