English
For any s, interior(s) ⊆ {x | gauge s x < 1}.
Русский
Для любой множества s interior(s) ⊆ {x : gauge s x < 1}.
LaTeX
$$$$\\operatorname{int}(s) \\subseteq \\{x \\mid \\mathrm{gauge}(s,x) < 1\\}.$$$$
Lean4
theorem interior_subset_gauge_lt_one (s : Set E) : interior s ⊆ {x | gauge s x < 1} :=
by
intro x hx
have H₁ : Tendsto (fun r : ℝ ↦ r⁻¹ • x) (𝓝[<] 1) (𝓝 ((1 : ℝ)⁻¹ • x)) :=
((tendsto_id.inv₀ one_ne_zero).smul tendsto_const_nhds).mono_left inf_le_left
rw [inv_one, one_smul] at H₁
have H₂ : ∀ᶠ r in 𝓝[<] (1 : ℝ), x ∈ r • s ∧ 0 < r ∧ r < 1 :=
by
filter_upwards [H₁ (mem_interior_iff_mem_nhds.1 hx), Ioo_mem_nhdsLT one_pos] with r h₁ h₂
exact ⟨(mem_smul_set_iff_inv_smul_mem₀ h₂.1.ne' _ _).2 h₁, h₂⟩
rcases H₂.exists with ⟨r, hxr, hr₀, hr₁⟩
exact (gauge_le_of_mem hr₀.le hxr).trans_lt hr₁
