𝕜 : Type u_1
𝕜₂ : Type ?u.228889
𝕝 : Type ?u.228892
𝕝₂ : Type ?u.228895
E : Type u_2
F : Type ?u.228901
G : Type ?u.228904
ι : Type u_3
ι' : Type ?u.228910
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ T1Space E → ∀ (x : E), x ≠ 0 → ∃ i, ↑(p i) x ≠ 0
𝕜 : Type u_1
𝕜₂ : Type ?u.228889
𝕝 : Type ?u.228892
𝕝₂ : Type ?u.228895
E : Type u_2
F : Type ?u.228901
G : Type ?u.228904
ι : Type u_3
ι' : Type ?u.228910
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ (∀ (x : E), x ≠ 0 → ∃ i, ↑(p i) x ≠ 0) ↔ T1Space E
refine' ⟨WithSeminorms.T1_of_separating hp, _⟩
𝕜 : Type u_1
𝕜₂ : Type ?u.228889
𝕝 : Type ?u.228892
𝕝₂ : Type ?u.228895
E : Type u_2
F : Type ?u.228901
G : Type ?u.228904
ι : Type u_3
ι' : Type ?u.228910
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
a✝ : T1Space E
⊢ ∀ (x : E), x ≠ 0 → ∃ i, ↑(p i) x ≠ 0
𝕜 : Type u_1
𝕜₂ : Type ?u.228889
𝕝 : Type ?u.228892
𝕝₂ : Type ?u.228895
E : Type u_2
F : Type ?u.228901
G : Type ?u.228904
ι : Type u_3
ι' : Type ?u.228910
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ T1Space E → ∀ (x : E), x ≠ 0 → ∃ i, ↑(p i) x ≠ 0
intro
no goals
𝕜 : Type u_1
𝕜₂ : Type ?u.228889
𝕝 : Type ?u.228892
𝕝₂ : Type ?u.228895
E : Type u_2
F : Type ?u.228901
G : Type ?u.228904
ι : Type u_3
ι' : Type ?u.228910
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
a✝ : T1Space E
⊢ ∀ (x : E), x ≠ 0 → ∃ i, ↑(p i) x ≠ 0
exact WithSeminorms.separating_of_T1 hp