instMinAbs — Mathlib

English

There is a canonical minimum operation on CauSeq(α, abs), defined pointwise by (f ∧ g)(n) = min(f(n), g(n)).

Русский

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

LaTeX

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

Lean4

instance : Min (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_inf_continuous_lemma (H₁ _ ij) (H₂ _ ij)⟩⟩

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