inf_limZero — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem inf_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_inf_iff.mpr ⟨H₁.1, H₂.1⟩, inf_lt_iff.mpr (Or.inl H₁.2)⟩

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