English
For any x in the scalar field and any basis U, there exists V ∈ p.addGroupFilterBasis.sets with V ⊆ preimage of U under the map y ↦ x•y.
Русский
Для любого x в скаляровой области и любого базисного U существует V ∈ p.addGroupFilterBasis.sets such that V ⊆ { y | x•y ∈ U }.
LaTeX
$$∃ V ∈ p.addGroupFilterBasis.sets, V ⊆ (fun y : F => x • y)^{-1} U$$
Lean4
theorem basisSets_smul_left (x : 𝕜) (U : Set F) (hU : U ∈ p.basisSets) :
∃ V ∈ p.addGroupFilterBasis.sets, V ⊆ (fun y : F => x • y) ⁻¹' U :=
by
rcases p.basisSets_iff.mp hU with ⟨s, r, hr, hU⟩
rw [hU]
by_cases h : x ≠ 0
· rw [(s.sup p).smul_ball_preimage 0 r x h, smul_zero]
use (s.sup p).ball 0 (r / ‖x‖)
exact ⟨p.basisSets_mem s (div_pos hr (norm_pos_iff.mpr h)), Subset.rfl⟩
refine ⟨(s.sup p).ball 0 r, p.basisSets_mem s hr, ?_⟩
simp only [not_ne_iff.mp h, Set.subset_def, mem_ball_zero, hr, mem_univ, map_zero, imp_true_iff,
preimage_const_of_mem, zero_smul]
