mono — Mathlib

English

If f =o[𝕜; l1] g and l2 ≤ l1, then f =o[𝕜; l2] g; monotonicity of little-OTVS with respect to the coarsening of the filter.

Русский

Если f =o[𝕜; l1] g и l2 ≤ l1, то f =o[𝕜; l2] g; монотонность отношения little-OTVS при упрощении фильтра.

LaTeX

$$$f =o[𝕜; l_1] g \\land l_2 \\le l_1 \\Rightarrow f =o[𝕜; l_2] g.$$$

Lean4

theorem mono (hf : f =o[𝕜; l₁] g) (h : l₂ ≤ l₁) : f =o[𝕜; l₂] g :=
  ⟨fun U hU ↦
    let ⟨V, hV0, hV⟩ := hf.1 U hU;
    ⟨V, hV0, fun ε hε ↦ (hV ε hε).filter_mono h⟩⟩

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