coe_sup — Mathlib

English

The coercion commutes with the pointwise supremum: the evaluation of f ⊔ g is the supremum of the evaluations.

Русский

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

LaTeX

$$$\\uparrow(f \\sqcup g) = \\uparrow f \\sqcup \\uparrow g$.$$

Lean4

@[simp, norm_cast]
theorem coe_sup (f g : C(α, β)) : ⇑(f ⊔ g) = ⇑f ⊔ g :=
  rfl

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