gauge_lt_of_mem_smul — Mathlib

English

If x ∈ ε · s with ε > 0, then gauge s x < ε.

Русский

Если x ∈ ε · s с ε > 0, тогда gauge s x < ε.

LaTeX

$$$$(\\text{IsOpen } s) \\Rightarrow (x \\in \\varepsilon \\cdot s) \\Rightarrow \\mathrm{gauge}(s,x) < \\varepsilon.$$$$

Lean4

theorem gauge_lt_of_mem_smul (x : E) (ε : ℝ) (hε : 0 < ε) (hs₂ : IsOpen s) (hx : x ∈ ε • s) : gauge s x < ε :=
  by
  have : ε⁻¹ • x ∈ s := by rwa [← mem_smul_set_iff_inv_smul_mem₀ hε.ne']
  have h_gauge_lt := gauge_lt_one_of_mem_of_isOpen hs₂ this
  rwa [gauge_smul_of_nonneg (inv_nonneg.2 hε.le), smul_eq_mul, inv_mul_lt_iff₀ hε, mul_one] at h_gauge_lt

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