coe_sup — Mathlib

English

The coercion of the pointwise sup equals the pointwise sup of the coercions: the function part of f ⊔ g is the join of f and g pointwise.

Русский

Приведение к функции сохраняет операцию верхнего предела по точкам: (f ⊔ g) как функция равен f(l) ⊔ g(l) для каждого аргумента.

LaTeX

$$$((f ⊔ g : α →o β) : α → β) = (f : α → β) ⊔ g$$$

Lean4

@[simp]
theorem coe_sup [SemilatticeSup β] (f g : α →o β) : ((f ⊔ g : α →o β) : α → β) = (f : α → β) ⊔ g :=
  rfl

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