English
The neighborhoods of zero have a basis consisting of balanced neighborhoods.
Русский
Окрестности нуля образуют базис, состоящий из сбалансированных окрестностей.
LaTeX
$$(𝓝 (0 : E)).HasBasis (fun s : Set E => s ∈ 𝓝 (0 : E) ∧ Balanced 𝕜 s) id$$
Lean4
theorem balancedCore_mem_nhds_zero (hU : U ∈ 𝓝 (0 : E)) : balancedCore 𝕜 U ∈ 𝓝 (0 : E) := by
-- Getting neighborhoods of the origin for `0 : 𝕜` and `0 : E`
obtain ⟨r, V, hr, hV, hrVU⟩ :
∃ (r : ℝ) (V : Set E), 0 < r ∧ V ∈ 𝓝 (0 : E) ∧ ∀ (c : 𝕜) (y : E), ‖c‖ < r → y ∈ V → c • y ∈ U :=
by
have h : Filter.Tendsto (fun x : 𝕜 × E => x.fst • x.snd) (𝓝 (0, 0)) (𝓝 0) :=
continuous_smul.tendsto' (0, 0) _ (smul_zero _)
simpa only [← Prod.exists', ← Prod.forall', ← and_imp, ← and_assoc, exists_prop] using
h.basis_left (NormedAddCommGroup.nhds_zero_basis_norm_lt.prod_nhds (𝓝 _).basis_sets) U hU
obtain ⟨y, hyr, hy₀⟩ : ∃ y : 𝕜, ‖y‖ < r ∧ y ≠ 0 :=
Filter.nonempty_of_mem <| (nhdsWithin_hasBasis NormedAddCommGroup.nhds_zero_basis_norm_lt {0}ᶜ).mem_of_mem hr
have : y • V ∈ 𝓝 (0 : E) := (set_smul_mem_nhds_zero_iff hy₀).mpr hV
refine Filter.mem_of_superset this (subset_balancedCore (mem_of_mem_nhds hU) fun a ha => ?_)
rw [smul_smul]
rintro _ ⟨z, hz, rfl⟩
refine hrVU _ _ ?_ hz
rw [norm_mul, ← one_mul r]
exact mul_lt_mul' ha hyr (norm_nonneg y) one_pos
