sup_limZero — Mathlib

English

If f and g have LimZero, then their pointwise maximum also has LimZero.

Русский

Если f и g имеют LimZero, то их точечный максимум тоже имеет LimZero.

LaTeX

$$$f.LimZero \to g.LimZero \to \mathrm{LimZero}(f \lor g).$$$

Lean4

theorem sup_limZero {f g : CauSeq α abs} (hf : LimZero f) (hg : LimZero g) : LimZero (f ⊔ g)
  | ε, ε0 =>
    (exists_forall_ge_and (hf _ ε0) (hg _ ε0)).imp fun _ H j ij =>
      by
      let ⟨H₁, H₂⟩ := H _ ij
      rw [abs_lt] at H₁ H₂ ⊢
      exact ⟨lt_sup_iff.mpr (Or.inl H₁.1), sup_lt_iff.mpr ⟨H₁.2, H₂.2⟩⟩

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