[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalAddGroup E
ι : Type u_3
b : ι → Set E
p : ι → Prop
hbasis : HasBasis (𝓝 0) p b
hconvex : ∀ (i : ι), p i → Convex 𝕜 (b i)
⊢ LocallyConvexSpace 𝕜 E
[PROOFSTEP]
refine'
  LocallyConvexSpace.ofBases 𝕜 E (fun (x : E) (i : ι) => (· + ·) x '' b i) (fun _ => p) (fun x => _) fun x i hi =>
    (hconvex i hi).translate x
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalAddGroup E
ι : Type u_3
b : ι → Set E
p : ι → Prop
hbasis : HasBasis (𝓝 0) p b
hconvex : ∀ (i : ι), p i → Convex 𝕜 (b i)
x : E
⊢ HasBasis (𝓝 x) ((fun x => p) x) ((fun x i => (fun x x_1 => x + x_1) x '' b i) x)
[PROOFSTEP]
rw [← map_add_left_nhds_zero]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalAddGroup E
ι : Type u_3
b : ι → Set E
p : ι → Prop
hbasis : HasBasis (𝓝 0) p b
hconvex : ∀ (i : ι), p i → Convex 𝕜 (b i)
x : E
⊢ HasBasis (map ((fun x x_1 => x + x_1) x) (𝓝 0)) ((fun x => p) x) ((fun x i => (fun x x_1 => x + x_1) x '' b i) x)
[PROOFSTEP]
exact hbasis.map _
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : LinearOrderedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed t
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v
[PROOFSTEP]
letI : UniformSpace E := TopologicalAddGroup.toUniformSpace E
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : LinearOrderedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed t
this : UniformSpace E := TopologicalAddGroup.toUniformSpace E
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v
[PROOFSTEP]
haveI : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : LinearOrderedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed t
this✝ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this : UniformAddGroup E
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v
[PROOFSTEP]
have := (LocallyConvexSpace.convex_open_basis_zero 𝕜 E).comap fun x : E × E => x.2 - x.1
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : LinearOrderedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed t
this✝¹ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝ : UniformAddGroup E
this :
  HasBasis (comap (fun x => x.snd - x.fst) (𝓝 0)) (fun s => 0 ∈ s ∧ IsOpen s ∧ Convex 𝕜 s) fun i =>
    (fun x => x.snd - x.fst) ⁻¹' id i
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v
[PROOFSTEP]
rw [← uniformity_eq_comap_nhds_zero] at this 
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : LinearOrderedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed t
this✝¹ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝ : UniformAddGroup E
this : HasBasis (uniformity E) (fun s => 0 ∈ s ∧ IsOpen s ∧ Convex 𝕜 s) fun i => (fun x => x.snd - x.fst) ⁻¹' id i
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v
[PROOFSTEP]
rcases disj.exists_uniform_thickening_of_basis this hs₂ ht₂ with ⟨V, ⟨hV0, hVopen, hVconvex⟩, hV⟩
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : LinearOrderedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed t
this✝¹ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝ : UniformAddGroup E
this : HasBasis (uniformity E) (fun s => 0 ∈ s ∧ IsOpen s ∧ Convex 𝕜 s) fun i => (fun x => x.snd - x.fst) ⁻¹' id i
V : Set E
hV :
  Disjoint (⋃ (x : E) (_ : x ∈ s), UniformSpace.ball x ((fun x => x.snd - x.fst) ⁻¹' id V))
    (⋃ (x : E) (_ : x ∈ t), UniformSpace.ball x ((fun x => x.snd - x.fst) ⁻¹' id V))
hV0 : 0 ∈ V
hVopen : IsOpen V
hVconvex : Convex 𝕜 V
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v
[PROOFSTEP]
refine'
  ⟨s + V, t + V, hVopen.add_left, hVopen.add_left, hs₁.add hVconvex, ht₁.add hVconvex, subset_add_left _ hV0,
    subset_add_left _ hV0, _⟩
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : LinearOrderedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed t
this✝¹ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝ : UniformAddGroup E
this : HasBasis (uniformity E) (fun s => 0 ∈ s ∧ IsOpen s ∧ Convex 𝕜 s) fun i => (fun x => x.snd - x.fst) ⁻¹' id i
V : Set E
hV :
  Disjoint (⋃ (x : E) (_ : x ∈ s), UniformSpace.ball x ((fun x => x.snd - x.fst) ⁻¹' id V))
    (⋃ (x : E) (_ : x ∈ t), UniformSpace.ball x ((fun x => x.snd - x.fst) ⁻¹' id V))
hV0 : 0 ∈ V
hVopen : IsOpen V
hVconvex : Convex 𝕜 V
⊢ Disjoint (s + V) (t + V)
[PROOFSTEP]
simp_rw [← iUnion_add_left_image, image_add_left]
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : LinearOrderedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed t
this✝¹ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝ : UniformAddGroup E
this : HasBasis (uniformity E) (fun s => 0 ∈ s ∧ IsOpen s ∧ Convex 𝕜 s) fun i => (fun x => x.snd - x.fst) ⁻¹' id i
V : Set E
hV :
  Disjoint (⋃ (x : E) (_ : x ∈ s), UniformSpace.ball x ((fun x => x.snd - x.fst) ⁻¹' id V))
    (⋃ (x : E) (_ : x ∈ t), UniformSpace.ball x ((fun x => x.snd - x.fst) ⁻¹' id V))
hV0 : 0 ∈ V
hVopen : IsOpen V
hVconvex : Convex 𝕜 V
⊢ Disjoint (⋃ (a : E) (_ : a ∈ s), (fun x => -a + x) ⁻¹' V) (⋃ (a : E) (_ : a ∈ t), (fun x => -a + x) ⁻¹' V)
[PROOFSTEP]
simp_rw [UniformSpace.ball, ← preimage_comp, sub_eq_neg_add] at hV 
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : LinearOrderedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed t
this✝¹ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝ : UniformAddGroup E
this : HasBasis (uniformity E) (fun s => 0 ∈ s ∧ IsOpen s ∧ Convex 𝕜 s) fun i => (fun x => x.snd - x.fst) ⁻¹' id i
V : Set E
hV0 : 0 ∈ V
hVopen : IsOpen V
hVconvex : Convex 𝕜 V
hV :
  Disjoint (⋃ (x : E) (_ : x ∈ s), (fun x => -x.fst + x.snd) ∘ Prod.mk x ⁻¹' id V)
    (⋃ (x : E) (_ : x ∈ t), (fun x => -x.fst + x.snd) ∘ Prod.mk x ⁻¹' id V)
⊢ Disjoint (⋃ (a : E) (_ : a ∈ s), (fun x => -a + x) ⁻¹' V) (⋃ (a : E) (_ : a ∈ t), (fun x => -a + x) ⁻¹' V)
[PROOFSTEP]
exact hV
[GOAL]
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
ts : Set (TopologicalSpace E)
h : ∀ (t : TopologicalSpace E), t ∈ ts → LocallyConvexSpace 𝕜 E
⊢ LocallyConvexSpace 𝕜 E
[PROOFSTEP]
letI : TopologicalSpace E := sInf ts
[GOAL]
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
ts : Set (TopologicalSpace E)
h : ∀ (t : TopologicalSpace E), t ∈ ts → LocallyConvexSpace 𝕜 E
this : TopologicalSpace E := sInf ts
⊢ LocallyConvexSpace 𝕜 E
[PROOFSTEP]
refine'
  LocallyConvexSpace.ofBases 𝕜 E (fun _ => fun If : Set ts × (ts → Set E) => ⋂ i ∈ If.1, If.2 i)
    (fun x => fun If : Set ts × (ts → Set E) => If.1.Finite ∧ ∀ i ∈ If.1, If.2 i ∈ @nhds _ (↑i) x ∧ Convex 𝕜 (If.2 i))
    (fun x => _) fun x If hif => convex_iInter fun i => convex_iInter fun hi => (hif.2 i hi).2
[GOAL]
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
ts : Set (TopologicalSpace E)
h : ∀ (t : TopologicalSpace E), t ∈ ts → LocallyConvexSpace 𝕜 E
this : TopologicalSpace E := sInf ts
x : E
⊢ HasBasis (𝓝 x)
    ((fun x If => Set.Finite If.fst ∧ ∀ (i : ↑ts), i ∈ If.fst → Prod.snd If i ∈ 𝓝 x ∧ Convex 𝕜 (Prod.snd If i)) x)
    ((fun x If => ⋂ (i : ↑ts) (_ : i ∈ If.fst), Prod.snd If i) x)
[PROOFSTEP]
rw [nhds_sInf, ← iInf_subtype'']
[GOAL]
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
ts : Set (TopologicalSpace E)
h : ∀ (t : TopologicalSpace E), t ∈ ts → LocallyConvexSpace 𝕜 E
this : TopologicalSpace E := sInf ts
x : E
⊢ HasBasis (⨅ (i : ↑ts), 𝓝 x)
    ((fun x If => Set.Finite If.fst ∧ ∀ (i : ↑ts), i ∈ If.fst → Prod.snd If i ∈ 𝓝 x ∧ Convex 𝕜 (Prod.snd If i)) x)
    ((fun x If => ⋂ (i : ↑ts) (_ : i ∈ If.fst), Prod.snd If i) x)
[PROOFSTEP]
exact hasBasis_iInf' fun i : ts => (@locallyConvexSpace_iff 𝕜 E _ _ _ ↑i).mp (h (↑i) i.2) x
[GOAL]
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
ts' : ι → TopologicalSpace E
h' : ∀ (i : ι), LocallyConvexSpace 𝕜 E
⊢ LocallyConvexSpace 𝕜 E
[PROOFSTEP]
refine' locallyConvexSpace_sInf _
[GOAL]
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
ts' : ι → TopologicalSpace E
h' : ∀ (i : ι), LocallyConvexSpace 𝕜 E
⊢ ∀ (t : TopologicalSpace E), (t ∈ range fun i => ts' i) → LocallyConvexSpace 𝕜 E
[PROOFSTEP]
rwa [forall_range_iff]
[GOAL]
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
t₁ t₂ : TopologicalSpace E
h₁ : LocallyConvexSpace 𝕜 E
h₂ : LocallyConvexSpace 𝕜 E
⊢ LocallyConvexSpace 𝕜 E
[PROOFSTEP]
rw [inf_eq_iInf]
[GOAL]
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
t₁ t₂ : TopologicalSpace E
h₁ : LocallyConvexSpace 𝕜 E
h₂ : LocallyConvexSpace 𝕜 E
⊢ LocallyConvexSpace 𝕜 E
[PROOFSTEP]
refine' locallyConvexSpace_iInf fun b => _
[GOAL]
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
t₁ t₂ : TopologicalSpace E
h₁ : LocallyConvexSpace 𝕜 E
h₂ : LocallyConvexSpace 𝕜 E
b : Bool
⊢ LocallyConvexSpace 𝕜 E
[PROOFSTEP]
cases b
[GOAL]
case false
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
t₁ t₂ : TopologicalSpace E
h₁ : LocallyConvexSpace 𝕜 E
h₂ : LocallyConvexSpace 𝕜 E
⊢ LocallyConvexSpace 𝕜 E
[PROOFSTEP]
assumption
[GOAL]
case true
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
t₁ t₂ : TopologicalSpace E
h₁ : LocallyConvexSpace 𝕜 E
h₂ : LocallyConvexSpace 𝕜 E
⊢ LocallyConvexSpace 𝕜 E
[PROOFSTEP]
assumption
[GOAL]
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
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
[PROOFSTEP]
letI : TopologicalSpace E := t.induced f
[GOAL]
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
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
[PROOFSTEP]
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
[GOAL]
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
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)
[PROOFSTEP]
rw [nhds_induced]
[GOAL]
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
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)
[PROOFSTEP]
exact (LocallyConvexSpace.convex_basis <| f x).comap f
