ι : Type u_1
R : Type u_2
A : Type ?u.38259
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB✝ hB : SubmodulesBasis B
this : TopologicalSpace M := topology hB
⊢ NonarchimedeanAddGroup M
ι : Type u_1
R : Type u_2
A : Type ?u.38259
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB✝ hB : SubmodulesBasis B
⊢ NonarchimedeanAddGroup M
letI := hB.topology
case is_nonarchimedean
ι : Type u_1
R : Type u_2
A : Type ?u.38259
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB✝ hB : SubmodulesBasis B
this : TopologicalSpace M := topology hB
⊢ ∀ (U : Set M), U ∈ 𝓝 0 → ∃ V, ↑V ⊆ U
ι : Type u_1
R : Type u_2
A : Type ?u.38259
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB✝ hB : SubmodulesBasis B
this : TopologicalSpace M := topology hB
⊢ NonarchimedeanAddGroup M
constructor
case is_nonarchimedean
ι : Type u_1
R : Type u_2
A : Type ?u.38259
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB✝ hB : SubmodulesBasis B
this : TopologicalSpace M := topology hB
U : Set M
hU : U ∈ 𝓝 0
⊢ ∃ V, ↑V ⊆ U
case is_nonarchimedean
ι : Type u_1
R : Type u_2
A : Type ?u.38259
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB✝ hB : SubmodulesBasis B
this : TopologicalSpace M := topology hB
⊢ ∀ (U : Set M), U ∈ 𝓝 0 → ∃ V, ↑V ⊆ U
intro U hU
case is_nonarchimedean.intro.intro.intro
ι : Type u_1
R : Type u_2
A : Type ?u.38259
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB✝ hB : SubmodulesBasis B
this : TopologicalSpace M := topology hB
U : Set M
hU : U ∈ 𝓝 0
i : ι
hi : ↑(B i) ⊆ U
⊢ ∃ V, ↑V ⊆ U
case is_nonarchimedean
ι : Type u_1
R : Type u_2
A : Type ?u.38259
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB✝ hB : SubmodulesBasis B
this : TopologicalSpace M := topology hB
U : Set M
hU : U ∈ 𝓝 0
⊢ ∃ V, ↑V ⊆ U
obtain ⟨-, ⟨i, rfl⟩, hi : (B i : Set M) ⊆ U⟩ :=
  hB.toModuleFilterBasis.toAddGroupFilterBasis.nhds_zero_hasBasis.mem_iff.mp hU
no goals
case is_nonarchimedean.intro.intro.intro
ι : Type u_1
R : Type u_2
A : Type ?u.38259
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB✝ hB : SubmodulesBasis B
this : TopologicalSpace M := topology hB
U : Set M
hU : U ∈ 𝓝 0
i : ι
hi : ↑(B i) ⊆ U
⊢ ∃ V, ↑V ⊆ U
exact ⟨hB.openAddSubgroup i, hi⟩