instMaxAbs — Mathlib

English

There is a canonical maximum operation on CauSeq(α, abs), defined pointwise by (f ⊔ g)(n) = max(f(n), g(n)).

Русский

Существует каноническое взятие максимума над CauSeq(α, abs), задаваемое (f ⊔ g)(n) = max(f(n), g(n)).

LaTeX

$$$\exists\!\text{max operation }\; (f,g)\mapsto f\lor g\text{ on } \mathrm{CauSeq}(\alpha,\mathrm{abs})\text{ with } (f\lor g)(n)=\max(f(n),g(n)).$$$

Lean4

instance : Max (CauSeq α abs) :=
  ⟨fun f g =>
    ⟨f ⊔ g, fun _ ε0 =>
      (exists_forall_ge_and (f.cauchy₃ ε0) (g.cauchy₃ ε0)).imp fun _ H _ ij =>
        let ⟨H₁, H₂⟩ := H _ le_rfl
        rat_sup_continuous_lemma (H₁ _ ij) (H₂ _ ij)⟩⟩

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