A_mono — Mathlib

English

If 0 < ε ≤ δ, then A(f, L, r, ε) ⊆ A(f, L, r, δ).

Русский

Если 0<ε≤δ, то A(f,L,r,ε) подмножество A(f,L,r,δ).

LaTeX

$$$$A(f,L,r,\varepsilon) \subseteq A(f,L,r,\delta)\quad\text{whenever } 0<\varepsilon\le\delta.$$$$

Lean4

theorem A_mono (L : E →L[𝕜] F) (r : ℝ) {ε δ : ℝ} (h : ε ≤ δ) : A f L r ε ⊆ A f L r δ :=
  by
  rintro x ⟨r', r'r, hr'⟩
  refine ⟨r', r'r, fun y hy z hz => (hr' y hy z hz).trans_le (mul_le_mul_of_nonneg_right h ?_)⟩
  linarith [mem_ball.1 hy, r'r.2, @dist_nonneg _ _ y x]

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