instMax — Mathlib

English

There is a maximum operation for SupBotHom α β defined coordinatewise by taking the maximum of the bottom and the maximum of the supers maps.

Русский

Существует операция максимума на SupBotHom(α,β), задаваемая покоординатно: максимум по нижмым функциям и максимум по верхним функциям.

LaTeX

$$$\\text{Max}_{\\mathrm{SupBotHom}(\\alpha,\\beta)}(f,g) := \\{ f_{\bot}\\lor g_{\bot},\\; (\\text{toSupHom}) = f_{\\text{sup}} \\lor g_{\\text{sup}} \\}$$$

Lean4

instance : Max (SupBotHom α β) :=
  ⟨fun f g => { f.toBotHom ⊔ g.toBotHom with toSupHom := f.toSupHom ⊔ g.toSupHom }⟩

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