Mathlib.Topology.Algebra.Module.LocallyConvex

LocallyConvexSpace structure

 (𝕜 E : Type*) [Semiring 𝕜] [PartialOrder 𝕜] [IsOrderedRing 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E]

Full source

/-- A `LocallyConvexSpace` is a topological semimodule over an ordered semiring in which convex
neighborhoods of a point form a neighborhood basis at that point. -/
class LocallyConvexSpace (𝕜 E : Type*) [Semiring 𝕜] [PartialOrder 𝕜] [IsOrderedRing 𝕜]
    [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] : Prop where
  convex_basis : ∀ x : E, (𝓝 x).HasBasis (fun s : Set E => s ∈ 𝓝 xs ∈ 𝓝 x ∧ Convex 𝕜 s) id

Locally Convex Space

Informal description

A locally convex space over an ordered semiring $\mathbb{K}$ is a topological semimodule $E$ where every point has a neighborhood basis consisting of convex sets. More precisely, for every point $x \in E$, the neighborhood filter $\mathcal{N}(x)$ has a basis of convex sets with respect to the ordered semiring $\mathbb{K}$.

locallyConvexSpace_iff theorem

: LocallyConvexSpace 𝕜 E ↔ ∀ x : E, (𝓝 x).HasBasis (fun s : Set E => s ∈ 𝓝 x ∧ Convex 𝕜 s) id

Full source

theorem locallyConvexSpace_iff :
    LocallyConvexSpaceLocallyConvexSpace 𝕜 E ↔ ∀ x : E, (𝓝 x).HasBasis (fun s : Set E => s ∈ 𝓝 x ∧ Convex 𝕜 s) id :=
  ⟨@LocallyConvexSpace.convex_basis _ _ _ _ _ _ _ _, LocallyConvexSpace.mk⟩

Characterization of Locally Convex Spaces via Convex Neighborhood Bases

Informal description

A topological semimodule $E$ over an ordered semiring $\mathbb{K}$ is a locally convex space if and only if for every point $x \in E$, the neighborhood filter $\mathcal{N}(x)$ has a basis consisting of convex sets. That is, for every $x \in E$, there exists a family of neighborhoods $\{s\}$ such that each $s$ is convex and belongs to $\mathcal{N}(x)$, and every neighborhood of $x$ contains some such $s$.

LocallyConvexSpace.ofBases theorem

 {ι : Type*} (b : E → ι → Set E) (p : E → ι → Prop) (hbasis : ∀ x : E, (𝓝 x).HasBasis (p x) (b x))
  (hconvex : ∀ x i, p x i → Convex 𝕜 (b x i)) : LocallyConvexSpace 𝕜 E

Full source

theorem LocallyConvexSpace.ofBases {ι : Type*} (b : E → ι → Set E) (p : E → ι → Prop)
    (hbasis : ∀ x : E, (𝓝 x).HasBasis (p x) (b x)) (hconvex : ∀ x i, p x i → Convex 𝕜 (b x i)) :
    LocallyConvexSpace 𝕜 E :=
  ⟨fun x =>
    (hbasis x).to_hasBasis
      (fun i hi => ⟨b x i, ⟨⟨(hbasis x).mem_of_mem hi, hconvex x i hi⟩, le_refl (b x i)⟩⟩)
      fun s hs =>
      ⟨(hbasis x).index s hs.1, ⟨(hbasis x).property_index hs.1, (hbasis x).set_index_subset hs.1⟩⟩⟩

Locally Convex Space Construction via Convex Neighborhood Bases

Informal description

Let $E$ be a topological semimodule over an ordered semiring $\mathbb{K}$. Suppose for each point $x \in E$, there exists an indexed family of sets $\{b(x,i)\}_{i \in \iota}$ and a predicate $p(x, \cdot) : \iota \to \text{Prop}$ such that: 1. The neighborhood filter $\mathcal{N}(x)$ has a basis consisting of the sets $b(x,i)$ where $p(x,i)$ holds. 2. For each $x \in E$ and $i \in \iota$, if $p(x,i)$ holds then $b(x,i)$ is convex. Then $E$ is a locally convex space over $\mathbb{K}$.

LocallyConvexSpace.convex_basis_zero theorem

[LocallyConvexSpace 𝕜 E] : (𝓝 0 : Filter E).HasBasis (fun s => s ∈ (𝓝 0 : Filter E) ∧ Convex 𝕜 s) id

Full source

theorem LocallyConvexSpace.convex_basis_zero [LocallyConvexSpace 𝕜 E] :
    (𝓝 0 : Filter E).HasBasis (fun s => s ∈ (𝓝 0 : Filter E)s ∈ (𝓝 0 : Filter E) ∧ Convex 𝕜 s) id :=
  LocallyConvexSpace.convex_basis 0

Neighborhood Basis of Zero in Locally Convex Space Consists of Convex Sets

Informal description

In a locally convex space $E$ over an ordered semiring $\mathbb{K}$, the neighborhood filter $\mathcal{N}(0)$ of the zero vector has a basis consisting of convex sets. That is, there exists a collection of convex sets $\{s\}$ such that a set $U$ is in $\mathcal{N}(0)$ if and only if $U$ contains some convex set $s$ from the basis.

locallyConvexSpace_iff_exists_convex_subset theorem

: LocallyConvexSpace 𝕜 E ↔ ∀ x : E, ∀ U ∈ 𝓝 x, ∃ S ∈ 𝓝 x, Convex 𝕜 S ∧ S ⊆ U

Full source

theorem locallyConvexSpace_iff_exists_convex_subset :
    LocallyConvexSpaceLocallyConvexSpace 𝕜 E ↔ ∀ x : E, ∀ U ∈ 𝓝 x, ∃ S ∈ 𝓝 x, Convex 𝕜 S ∧ S ⊆ U :=
  (locallyConvexSpace_iff 𝕜 E).trans (forall_congr' fun _ => hasBasis_self)

Characterization of Locally Convex Spaces via Convex Neighborhood Subsets

Informal description

A topological semimodule $E$ over an ordered semiring $\mathbb{K}$ is a locally convex space if and only if for every point $x \in E$ and every neighborhood $U$ of $x$, there exists a convex neighborhood $S$ of $x$ such that $S \subseteq U$.

LocallyConvexSpace.ofBasisZero theorem

 {ι : Type*} (b : ι → Set E) (p : ι → Prop) (hbasis : (𝓝 0).HasBasis p b) (hconvex : ∀ i, p i → Convex 𝕜 (b i)) :
  LocallyConvexSpace 𝕜 E

Full source

theorem LocallyConvexSpace.ofBasisZero {ι : Type*} (b : ι → Set E) (p : ι → Prop)
    (hbasis : (𝓝 0).HasBasis p b) (hconvex : ∀ i, p i → Convex 𝕜 (b i)) :
    LocallyConvexSpace 𝕜 E := by
  refine LocallyConvexSpace.ofBases 𝕜 E (fun (x : E) (i : ι) => (x + ·) '' b i) (fun _ => p)
    (fun x => ?_) fun x i hi => (hconvex i hi).translate x
  rw [← map_add_left_nhds_zero]
  exact hbasis.map _

Construction of Locally Convex Space via Convex Neighborhood Basis at Zero

Informal description

Let $E$ be a topological semimodule over an ordered semiring $\mathbb{K}$. Suppose there exists an indexed family of sets $\{b_i\}_{i \in \iota}$ and a predicate $p : \iota \to \text{Prop}$ such that: 1. The neighborhood filter $\mathcal{N}(0)$ of the zero vector has a basis consisting of the sets $b_i$ where $p(i)$ holds. 2. For each $i \in \iota$, if $p(i)$ holds then $b_i$ is convex. Then $E$ is a locally convex space over $\mathbb{K}$.

locallyConvexSpace_iff_zero theorem

 : LocallyConvexSpace 𝕜 E ↔ (𝓝 0 : Filter E).HasBasis (fun s : Set E => s ∈ (𝓝 0 : Filter E) ∧ Convex 𝕜 s) id

Full source

theorem locallyConvexSpace_iff_zero : LocallyConvexSpaceLocallyConvexSpace 𝕜 E ↔
    (𝓝 0 : Filter E).HasBasis (fun s : Set E => s ∈ (𝓝 0 : Filter E) ∧ Convex 𝕜 s) id :=
  ⟨fun _ => LocallyConvexSpace.convex_basis 0, fun h =>
    LocallyConvexSpace.ofBasisZero 𝕜 E _ _ h fun _ => And.right⟩

Characterization of Locally Convex Spaces via Convex Neighborhood Basis at Zero

Informal description

A topological semimodule $E$ over an ordered semiring $\mathbb{K}$ is a locally convex space if and only if the neighborhood filter $\mathcal{N}(0)$ of the zero vector has a basis consisting of convex sets. More precisely, there exists a basis for $\mathcal{N}(0)$ where each set in the basis is both a neighborhood of $0$ and convex with respect to $\mathbb{K}$.

locallyConvexSpace_iff_exists_convex_subset_zero theorem

: LocallyConvexSpace 𝕜 E ↔ ∀ U ∈ (𝓝 0 : Filter E), ∃ S ∈ (𝓝 0 : Filter E), Convex 𝕜 S ∧ S ⊆ U

Full source

theorem locallyConvexSpace_iff_exists_convex_subset_zero :
    LocallyConvexSpaceLocallyConvexSpace 𝕜 E ↔ ∀ U ∈ (𝓝 0 : Filter E), ∃ S ∈ (𝓝 0 : Filter E), Convex 𝕜 S ∧ S ⊆ U :=
  (locallyConvexSpace_iff_zero 𝕜 E).trans hasBasis_self

Characterization of Locally Convex Spaces via Convex Subsets of Neighborhoods at Zero

Informal description

A topological semimodule $E$ over an ordered semiring $\mathbb{K}$ is a locally convex space if and only if for every neighborhood $U$ of $0$ in $E$, there exists a convex neighborhood $S$ of $0$ such that $S \subseteq U$.

LocallyConvexSpace.toLocPathConnectedSpace instance

[Module ℝ E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] : LocPathConnectedSpace E

Full source

instance (priority := 100) LocallyConvexSpace.toLocPathConnectedSpace [Module ℝ E]
    [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] : LocPathConnectedSpace E :=
  .of_bases (fun x ↦ convex_basis (𝕜 := ℝ) x)
    fun _ _ hs ↦ hs.2.isPathConnected <| nonempty_of_mem <| mem_of_mem_nhds hs.1

Local Path-Connectedness of Locally Convex Spaces over ℝ

Informal description

Every locally convex space $E$ over the real numbers with continuous scalar multiplication is locally path-connected.

Convex.locPathConnectedSpace theorem

 [Module ℝ E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {S : Set E} (hS : Convex ℝ S) : LocPathConnectedSpace S

Full source

/-- Convex subsets of locally convex spaces are locally path-connected. -/
theorem Convex.locPathConnectedSpace [Module ℝ E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E]
    {S : Set E} (hS : Convex ℝ S) : LocPathConnectedSpace S := by
  refine ⟨fun x ↦ ⟨fun s ↦ ⟨fun hs ↦ ?_, fun ⟨t, ht⟩ ↦ mem_of_superset ht.1.1 ht.2⟩⟩⟩
  let ⟨t, ht⟩ := (mem_nhds_subtype S x s).mp hs
  let ⟨t', ht'⟩ := (LocallyConvexSpace.convex_basis (𝕜 := ℝ) x.1).mem_iff.mp ht.1
  refine ⟨(↑) ⁻¹' t', ⟨?_, ?_⟩, (preimage_mono ht'.2).trans ht.2⟩
  · exact continuousAt_subtype_val.preimage_mem_nhds ht'.1.1
  · refine Subtype.preimage_coe_self_inter _ _ ▸ IsPathConnected.preimage_coe ?_ inter_subset_left
    exact (hS.inter ht'.1.2).isPathConnected ⟨x, x.2, mem_of_mem_nhds ht'.1.1⟩

Local Path-Connectedness of Convex Subsets in Locally Convex Real Topological Vector Spaces

Informal description

Let $E$ be a real topological vector space that is locally convex. For any convex subset $S \subseteq E$, the subspace $S$ is locally path-connected.

LocallyConvexSpace.convex_open_basis_zero theorem

[LocallyConvexSpace 𝕜 E] : (𝓝 0 : Filter E).HasBasis (fun s => (0 : E) ∈ s ∧ IsOpen s ∧ Convex 𝕜 s) id

Full source

theorem LocallyConvexSpace.convex_open_basis_zero [LocallyConvexSpace 𝕜 E] :
    (𝓝 0 : Filter E).HasBasis (fun s => (0 : E) ∈ s(0 : E) ∈ s ∧ IsOpen s ∧ Convex 𝕜 s) id :=
  (LocallyConvexSpace.convex_basis_zero 𝕜 E).to_hasBasis
    (fun s hs =>
      ⟨interior s, ⟨mem_interior_iff_mem_nhds.mpr hs.1, isOpen_interior, hs.2.interior⟩,
        interior_subset⟩)
    fun s hs => ⟨s, ⟨hs.2.1.mem_nhds hs.1, hs.2.2⟩, subset_rfl⟩

Neighborhood Basis of Zero in Locally Convex Space Consists of Open Convex Sets

Informal description

In a locally convex space $E$ over an ordered semiring $\mathbb{K}$, the neighborhood filter $\mathcal{N}(0)$ of the zero vector has a basis consisting of open convex sets containing $0$. That is, a set $U$ is in $\mathcal{N}(0)$ if and only if there exists an open convex set $s$ containing $0$ such that $s \subseteq U$.

Disjoint.exists_open_convexes theorem

 [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

Full source

/-- In a locally convex space, if `s`, `t` are disjoint convex sets, `s` is compact and `t` is
closed, then we can find open disjoint convex sets containing them. -/
theorem Disjoint.exists_open_convexes [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 := by
  letI : UniformSpace E := IsTopologicalAddGroup.toUniformSpace E
  haveI : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup
  have := (LocallyConvexSpace.convex_open_basis_zero 𝕜 E).comap fun x : E × E => x.2 - x.1
  rw [← uniformity_eq_comap_nhds_zero] at this
  rcases disj.exists_uniform_thickening_of_basis this hs₂ ht₂ with ⟨V, ⟨hV0, hVopen, hVconvex⟩, hV⟩
  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, ?_⟩
  simp_rw [← iUnion_add_left_image, image_add_left]
  simp_rw [UniformSpace.ball, ← preimage_comp, sub_eq_neg_add] at hV
  exact hV

Separation of Disjoint Compact and Closed Convex Sets in Locally Convex Spaces

Informal description

Let $E$ be a locally convex space over an ordered semiring $\mathbb{K}$. For any two disjoint convex subsets $s$ and $t$ of $E$, where $s$ is compact and $t$ is closed, there exist open convex subsets $u$ and $v$ of $E$ such that $s \subseteq u$, $t \subseteq v$, and $u$ and $v$ are disjoint.

locallyConvexSpace_sInf theorem

 {ts : Set (TopologicalSpace E)} (h : ∀ t ∈ ts, @LocallyConvexSpace 𝕜 E _ _ _ _ _ t) :
  @LocallyConvexSpace 𝕜 E _ _ _ _ _ (sInf ts)

Full source

theorem locallyConvexSpace_sInf {ts : Set (TopologicalSpace E)}
    (h : ∀ t ∈ ts, @LocallyConvexSpace 𝕜 E _ _ _ _ _ t) :
    @LocallyConvexSpace 𝕜 E _ _ _ _ _ (sInf ts) := by
  letI : TopologicalSpace E := sInf ts
  refine
    LocallyConvexSpace.ofBases 𝕜 E (fun _ => fun If : SetSet ts × (ts → Set E) => ⋂ i ∈ If.1, If.2 i)
      (fun x => fun If : SetSet 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
  rw [nhds_sInf, ← iInf_subtype'']
  exact hasBasis_iInf' fun i : ts => (@locallyConvexSpace_iff 𝕜 E _ _ _ _ _ ↑i).mp (h (↑i) i.2) x

Infimum of Locally Convex Topologies is Locally Convex

Informal description

Let $E$ be a module over an ordered semiring $\mathbb{K}$ and let $\{t_i\}_{i \in I}$ be a collection of topologies on $E$. If each topology $t_i$ makes $E$ a locally convex space over $\mathbb{K}$, then the infimum topology $\bigsqcap_{i \in I} t_i$ also makes $E$ a locally convex space over $\mathbb{K}$.

locallyConvexSpace_iInf theorem

 {ts' : ι → TopologicalSpace E} (h' : ∀ i, @LocallyConvexSpace 𝕜 E _ _ _ _ _ (ts' i)) :
  @LocallyConvexSpace 𝕜 E _ _ _ _ _ (⨅ i, ts' i)

Full source

theorem locallyConvexSpace_iInf {ts' : ι → TopologicalSpace E}
    (h' : ∀ i, @LocallyConvexSpace 𝕜 E _ _ _ _ _ (ts' i)) :
    @LocallyConvexSpace 𝕜 E _ _ _ _ _ (⨅ i, ts' i) := by
  refine locallyConvexSpace_sInf ?_
  rwa [forall_mem_range]

Infimum of Locally Convex Topologies is Locally Convex

Informal description

Let $E$ be a module over an ordered semiring $\mathbb{K}$ and let $\{t_i\}_{i \in I}$ be a family of topologies on $E$. If each topology $t_i$ makes $E$ a locally convex space over $\mathbb{K}$, then the infimum topology $\bigsqcap_{i \in I} t_i$ also makes $E$ a locally convex space over $\mathbb{K}$.

locallyConvexSpace_inf theorem

 {t₁ t₂ : TopologicalSpace E} (h₁ : @LocallyConvexSpace 𝕜 E _ _ _ _ _ t₁) (h₂ : @LocallyConvexSpace 𝕜 E _ _ _ _ _ t₂) :
  @LocallyConvexSpace 𝕜 E _ _ _ _ _ (t₁ ⊓ t₂)

Full source

theorem locallyConvexSpace_inf {t₁ t₂ : TopologicalSpace E}
    (h₁ : @LocallyConvexSpace 𝕜 E _ _ _ _ _ t₁)
    (h₂ : @LocallyConvexSpace 𝕜 E _ _ _ _ _ t₂) : @LocallyConvexSpace 𝕜 E _ _ _ _ _ (t₁ ⊓ t₂) := by
  rw [inf_eq_iInf]
  refine locallyConvexSpace_iInf fun b => ?_
  cases b <;> assumption

Infimum of Two Locally Convex Topologies is Locally Convex

Informal description

Let $E$ be a module over an ordered semiring $\mathbb{K}$ equipped with two topologies $t_1$ and $t_2$. If both $t_1$ and $t_2$ make $E$ a locally convex space over $\mathbb{K}$, then the infimum topology $t_1 \sqcap t_2$ (the coarsest topology finer than both $t_1$ and $t_2$) also makes $E$ a locally convex space over $\mathbb{K}$.

locallyConvexSpace_induced theorem

 {t : TopologicalSpace F} [LocallyConvexSpace 𝕜 F] (f : E →ₗ[𝕜] F) : @LocallyConvexSpace 𝕜 E _ _ _ _ _ (t.induced f)

Full source

theorem locallyConvexSpace_induced {t : TopologicalSpace F} [LocallyConvexSpace 𝕜 F]
    (f : E →ₗ[𝕜] F) : @LocallyConvexSpace 𝕜 E _ _ _ _ _ (t.induced f) := by
  letI : TopologicalSpace E := t.induced f
  refine LocallyConvexSpace.ofBases 𝕜 E (fun _ => preimage f)
    (fun x => fun s : Set F => s ∈ 𝓝 (f x)s ∈ 𝓝 (f x) ∧ Convex 𝕜 s) (fun x => ?_) fun x s ⟨_, hs⟩ =>
    hs.linear_preimage f
  rw [nhds_induced]
  exact (LocallyConvexSpace.convex_basis <| f x).comap f

Induced Locally Convex Topology under Linear Maps

Informal description

Let $E$ and $F$ be topological semimodules over an ordered semiring $\mathbb{K}$, with $F$ being locally convex. Given a linear map $f : E \to F$, the induced topology on $E$ (where open sets are preimages of open sets in $F$ under $f$) makes $E$ a locally convex space over $\mathbb{K}$.

Pi.locallyConvexSpace instance

 {ι : Type*} {X : ι → Type*} [∀ i, AddCommMonoid (X i)] [∀ i, TopologicalSpace (X i)] [∀ i, Module 𝕜 (X i)]
  [∀ i, LocallyConvexSpace 𝕜 (X i)] : LocallyConvexSpace 𝕜 (∀ i, X i)

Full source

instance Pi.locallyConvexSpace {ι : Type*} {X : ι → Type*} [∀ i, AddCommMonoid (X i)]
    [∀ i, TopologicalSpace (X i)] [∀ i, Module 𝕜 (X i)] [∀ i, LocallyConvexSpace 𝕜 (X i)] :
    LocallyConvexSpace 𝕜 (∀ i, X i) :=
  locallyConvexSpace_iInf fun i => locallyConvexSpace_induced (LinearMap.proj i)

Locally Convex Structure on Product Spaces

Informal description

For any family of topological modules $\{X_i\}_{i \in \iota}$ over an ordered semiring $\mathbb{K}$, where each $X_i$ is a locally convex space, the product space $\prod_{i \in \iota} X_i$ equipped with the product topology is also a locally convex space over $\mathbb{K}$.

Prod.locallyConvexSpace instance

 [TopologicalSpace E] [TopologicalSpace F] [LocallyConvexSpace 𝕜 E] [LocallyConvexSpace 𝕜 F] :
  LocallyConvexSpace 𝕜 (E × F)

Full source

instance Prod.locallyConvexSpace [TopologicalSpace E] [TopologicalSpace F] [LocallyConvexSpace 𝕜 E]
    [LocallyConvexSpace 𝕜 F] : LocallyConvexSpace 𝕜 (E × F) :=
  locallyConvexSpace_inf
    (locallyConvexSpace_induced (LinearMap.fst _ _ _))
    (locallyConvexSpace_induced (LinearMap.snd _ _ _))

Locally Convex Structure on Product Spaces

Informal description

For any two topological modules $E$ and $F$ over an ordered semiring $\mathbb{K}$, if both $E$ and $F$ are locally convex spaces, then the product space $E \times F$ equipped with the product topology is also a locally convex space over $\mathbb{K}$.

LinearOrderedSemiring.toLocallyConvexSpace instance

 {R : Type*} [TopologicalSpace R] [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] [OrderTopology R] :
  LocallyConvexSpace R R

Full source

instance LinearOrderedSemiring.toLocallyConvexSpace {R : Type*} [TopologicalSpace R]
    [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] [OrderTopology R] :
    LocallyConvexSpace R R where
  convex_basis x := by
    obtain hl | hl := isBot_or_exists_lt x
    · refine hl.rec ?_ _
      intro
      refine nhds_bot_basis.to_hasBasis' ?_ ?_
      · intros
        refine ⟨Set.Iio _, ?_, .rfl⟩
        simp_all [Iio_mem_nhds, convex_Iio]
      · simp +contextual
    obtain hu | hu := isTop_or_exists_gt x
    · refine hu.rec ?_ _
      intro
      refine nhds_top_basis.to_hasBasis' ?_ ?_
      · intros
        refine ⟨Set.Ioi _, ?_, subset_refl _⟩
        simp_all [Ioi_mem_nhds, convex_Ioi]
      · simp +contextual
    refine (nhds_basis_Ioo' hl hu).to_hasBasis' ?_ ?_
    · simp only [id_eq, and_imp, Prod.forall]
      intros
      refine ⟨_, ?_, subset_refl _⟩
      simp_all [Ioo_mem_nhds, convex_Ioo]
    · simp +contextual

Linearly Ordered Semirings as Locally Convex Spaces

Informal description

Every linearly ordered semiring $R$ with a strict ordered ring structure and the order topology is a locally convex space over itself. This means that for every point in $R$, there exists a neighborhood basis consisting of convex sets.

Convex.eventually_nhdsWithin_segment theorem

 {E 𝕜 : Type*} [Semiring 𝕜] [PartialOrder 𝕜] [IsOrderedRing 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E]
  [LocallyConvexSpace 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) {x₀ : E} (hx₀s : x₀ ∈ s) {p : E → Prop}
  (h : ∀ᶠ x in 𝓝[s] x₀, p x) : ∀ᶠ x in 𝓝[s] x₀, ∀ y ∈ segment 𝕜 x₀ x, p y

Full source

lemma Convex.eventually_nhdsWithin_segment {E 𝕜 : Type*}
    [Semiring 𝕜] [PartialOrder 𝕜] [IsOrderedRing 𝕜]
    [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [LocallyConvexSpace 𝕜 E]
    {s : Set E} (hs : Convex 𝕜 s) {x₀ : E} (hx₀s : x₀ ∈ s)
    {p : E → Prop} (h : ∀ᶠ x in 𝓝[s] x₀, p x) :
    ∀ᶠ x in 𝓝[s] x₀, ∀ y ∈ segment 𝕜 x₀ x, p y := by
  rw [eventually_nhdsWithin_iff, (LocallyConvexSpace.convex_basis (𝕜 := 𝕜) x₀).eventually_iff]
    at h ⊢
  obtain ⟨u, ⟨hu_nhds, hu_convex⟩, h⟩ := h
  refine ⟨u, ⟨hu_nhds, hu_convex⟩, fun x hxu hxs y hy ↦ h ?_ (hs.segment_subset hx₀s hxs hy)⟩
  suffices segmentsegment 𝕜 x₀ x ⊆ u from this hy
  exact hu_convex.segment_subset (mem_of_mem_nhds hu_nhds) hxu

Neighborhood Property Propagation Along Segments in Locally Convex Spaces

Informal description

Let $E$ be a topological module over an ordered semiring $\mathbb{K}$ that is locally convex. Let $s \subseteq E$ be a convex set containing a point $x_0 \in s$, and let $p$ be a predicate on $E$. If $p(x)$ holds for all $x$ in a neighborhood of $x_0$ within $s$, then for all $x$ in a neighborhood of $x_0$ within $s$, the predicate $p(y)$ holds for every $y$ in the closed segment connecting $x_0$ and $x$.

Mathlib.Topology.Algebra.Module.LocallyConvex

Main results

TODO