basisSets_smul_right — Mathlib

English

For any v ∈ E and any basis U, there exists a neighborhood V of 0 in R and W in the basis such that V·W ⊆ U.

Русский

Для любого v ∈ E и любого базисного множества U существует окрестность V нуля в R и W в базисе так, что V·W ⊆ U.

LaTeX

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

Lean4

theorem basisSets_smul_right (v : E) (U : Set E) (hU : U ∈ p.basisSets) : ∀ᶠ x : R in 𝓝 0, x • v ∈ U :=
  by
  rcases p.basisSets_iff.mp hU with ⟨s, r, hr, hU⟩
  rw [hU, Filter.eventually_iff]
  simp_rw [(s.sup p).mem_ball_zero, map_smul_eq_mul]
  by_cases h : 0 < (s.sup p) v
  · simp_rw [(lt_div_iff₀ h).symm]
    rw [← _root_.ball_zero_eq]
    exact Metric.ball_mem_nhds 0 (div_pos hr h)
  simp_rw [le_antisymm (not_lt.mp h) (apply_nonneg _ v), mul_zero, hr]
  exact IsOpen.mem_nhds isOpen_univ (mem_univ 0)

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