ι : Type u_3
R : Type u_1
A : Type ?u.51903
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
BR : RingFilterBasis R
B : ι → Submodule R M
hB : SubmodulesBasis BR B
x✝ : TopologicalSpace R := topology BR
this : TopologicalSpace R := topology BR
⊢ ∀ (m : M) (i : ι), ∀ᶠ (a : R) in 𝓝 0, a • m ∈ B i
ι : Type u_3
R : Type u_1
A : Type ?u.51903
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
BR : RingFilterBasis R
B : ι → Submodule R M
hB : SubmodulesBasis BR B
x✝ : TopologicalSpace R := topology BR
⊢ ∀ (m : M) (i : ι), ∀ᶠ (a : R) in 𝓝 0, a • m ∈ B i
letI := BR.topology
ι : Type u_3
R : Type u_1
A : Type ?u.51903
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
BR : RingFilterBasis R
B : ι → Submodule R M
hB : SubmodulesBasis BR B
x✝ : TopologicalSpace R := topology BR
this : TopologicalSpace R := topology BR
m : M
i : ι
⊢ ∀ᶠ (a : R) in 𝓝 0, a • m ∈ B i
ι : Type u_3
R : Type u_1
A : Type ?u.51903
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
BR : RingFilterBasis R
B : ι → Submodule R M
hB : SubmodulesBasis BR B
x✝ : TopologicalSpace R := topology BR
this : TopologicalSpace R := topology BR
⊢ ∀ (m : M) (i : ι), ∀ᶠ (a : R) in 𝓝 0, a • m ∈ B i
intro m i
case intro.intro
ι : Type u_3
R : Type u_1
A : Type ?u.51903
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
BR : RingFilterBasis R
B : ι → Submodule R M
hB : SubmodulesBasis BR B
x✝ : TopologicalSpace R := topology BR
this : TopologicalSpace R := topology BR
m : M
i : ι
V : Set R
V_in : V ∈ BR
hV : V ⊆ (fun x => x • m) ⁻¹' ↑(B i)
⊢ ∀ᶠ (a : R) in 𝓝 0, a • m ∈ B i
ι : Type u_3
R : Type u_1
A : Type ?u.51903
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
BR : RingFilterBasis R
B : ι → Submodule R M
hB : SubmodulesBasis BR B
x✝ : TopologicalSpace R := topology BR
this : TopologicalSpace R := topology BR
m : M
i : ι
⊢ ∀ᶠ (a : R) in 𝓝 0, a • m ∈ B i
rcases hB.smul m i with ⟨V, V_in, hV⟩
no goals
case intro.intro
ι : Type u_3
R : Type u_1
A : Type ?u.51903
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
BR : RingFilterBasis R
B : ι → Submodule R M
hB : SubmodulesBasis BR B
x✝ : TopologicalSpace R := topology BR
this : TopologicalSpace R := topology BR
m : M
i : ι
V : Set R
V_in : V ∈ BR
hV : V ⊆ (fun x => x • m) ⁻¹' ↑(B i)
⊢ ∀ᶠ (a : R) in 𝓝 0, a • m ∈ B i
exact mem_of_superset (BR.toAddGroupFilterBasis.mem_nhds_zero V_in) hV