ι : Sort ?u.45774
𝕜 : Type u_2
E : Type u_3
F : Type u_1
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
t : TopologicalSpace F
inst✝ : LocallyConvexSpace 𝕜 F
f : E →ₗ[𝕜] F
this : TopologicalSpace E := induced (↑f) t
⊢ LocallyConvexSpace 𝕜 E
ι : Sort ?u.45774
𝕜 : Type u_2
E : Type u_3
F : Type u_1
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
t : TopologicalSpace F
inst✝ : LocallyConvexSpace 𝕜 F
f : E →ₗ[𝕜] F
⊢ LocallyConvexSpace 𝕜 E
letI : TopologicalSpace E := t.induced f
ι : Sort ?u.45774
𝕜 : Type u_2
E : Type u_3
F : Type u_1
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
t : TopologicalSpace F
inst✝ : LocallyConvexSpace 𝕜 F
f : E →ₗ[𝕜] F
this : TopologicalSpace E := induced (↑f) t
x : E
⊢ HasBasis (𝓝 x) ((fun x s => s ∈ 𝓝 (↑f x) ∧ Convex 𝕜 s) x) ((fun x => preimage ↑f) x)
ι : Sort ?u.45774
𝕜 : Type u_2
E : Type u_3
F : Type u_1
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
t : TopologicalSpace F
inst✝ : LocallyConvexSpace 𝕜 F
f : E →ₗ[𝕜] F
this : TopologicalSpace E := induced (↑f) t
⊢ LocallyConvexSpace 𝕜 E
refine' LocallyConvexSpace.ofBases 𝕜 E (fun _ => preimage f)
  (fun x => fun s : Set F => s ∈ 𝓝 (f x) ∧ Convex 𝕜 s) (fun x => _) fun x s ⟨_, hs⟩ =>
  hs.linear_preimage f
ι : Sort ?u.45774
𝕜 : Type u_2
E : Type u_3
F : Type u_1
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
t : TopologicalSpace F
inst✝ : LocallyConvexSpace 𝕜 F
f : E →ₗ[𝕜] F
this : TopologicalSpace E := induced (↑f) t
x : E
⊢ HasBasis (comap (↑f) (𝓝 (↑f x))) ((fun x s => s ∈ 𝓝 (↑f x) ∧ Convex 𝕜 s) x) ((fun x => preimage ↑f) x)
ι : Sort ?u.45774
𝕜 : Type u_2
E : Type u_3
F : Type u_1
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
t : TopologicalSpace F
inst✝ : LocallyConvexSpace 𝕜 F
f : E →ₗ[𝕜] F
this : TopologicalSpace E := induced (↑f) t
x : E
⊢ HasBasis (𝓝 x) ((fun x s => s ∈ 𝓝 (↑f x) ∧ Convex 𝕜 s) x) ((fun x => preimage ↑f) x)
rw [nhds_induced]
no goals
ι : Sort ?u.45774
𝕜 : Type u_2
E : Type u_3
F : Type u_1
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
t : TopologicalSpace F
inst✝ : LocallyConvexSpace 𝕜 F
f : E →ₗ[𝕜] F
this : TopologicalSpace E := induced (↑f) t
x : E
⊢ HasBasis (comap (↑f) (𝓝 (↑f x))) ((fun x s => s ∈ 𝓝 (↑f x) ∧ Convex 𝕜 s) x) ((fun x => preimage ↑f) x)
exact (LocallyConvexSpace.convex_basis <| f x).comap f