basisSets_smul — Mathlib

English

For every U in the basis, there exist V ∈ 𝓝(0_R) and W ∈ p.addGroupFilterBasis.sets with V·W ⊆ U.

Русский

Для любого U в базе существуют V ∈ 𝓝(0_R) и W ∈ p.addGroupFilterBasis.sets с V·W ⊆ U.

LaTeX

$$∃ V ∈ 𝓝(0_R), ∃ W ∈ p.addGroupFilterBasis.sets, V • W ⊆ U$$

Lean4

theorem basisSets_smul (U) (hU : U ∈ p.basisSets) : ∃ V ∈ 𝓝 (0 : R), ∃ W ∈ p.addGroupFilterBasis.sets, V • W ⊆ U :=
  by
  rcases p.basisSets_iff.mp hU with ⟨s, r, hr, hU⟩
  refine ⟨Metric.ball 0 √r, Metric.ball_mem_nhds 0 (Real.sqrt_pos.mpr hr), ?_⟩
  refine ⟨(s.sup p).ball 0 √r, p.basisSets_mem s (Real.sqrt_pos.mpr hr), ?_⟩
  refine Set.Subset.trans (ball_smul_ball (s.sup p) √r √r) ?_
  rw [hU, Real.mul_self_sqrt (le_of_lt hr)]

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