coe_sup — Mathlib

English

The notation and lifting to functions commute with sup: the underlying function of f ⊔ g equals the pointwise max of f and g.

Русский

Обозначение и переход к функциям сохраняют операцию sup: соответствующая функция для f ⊔ g равна точечному максимуму.

LaTeX

$$$\uparrow(f \lor g)(n)=\max\{f(n),g(n)\}\quad(\forall n).$$$

Lean4

@[simp, norm_cast]
theorem coe_sup (f g : CauSeq α abs) : ⇑(f ⊔ g) = (f : ℕ → α) ⊔ g :=
  rfl

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