sup_eq_map₂ — Mathlib

English

The pointwise supremum of two simple functions equals the map of their pair via the sup operation: f ⊔ g = (pair f g).map (λ p, p.1 ⊔ p.2).

Русский

Покоя верхняя ограда двух простых функций равна отображению пары функций через операцию верхней ограды: f ⊔ g = (pair f g).map (λ p, p.1 ⊔ p.2).

LaTeX

$$$f \\sqcup g = (\\text{pair } f\\ g).\\text{map } (\\lambda p:(\\beta \\times \\beta), p.1 \\sqcup p.2).$$$

Lean4

theorem sup_eq_map₂ [Max β] (f g : α →ₛ β) : f ⊔ g = (pair f g).map fun p : β × β => p.1 ⊔ p.2 :=
  rfl

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