toLocallyConvexSpace — Mathlib

English

A linear ordered semiring R is a locally convex space over itself (R as an R-module).

Русский

Линейно упорядоченная полуприводная полукольцевая структура R является локально выпуклым пространством над самой собой (как модуль над R).

LaTeX

$$$\text{LocallyConvexSpace } R R$$$

Lean4

/-- A linear ordered semiring is a locally convex space over itself. -/
instance 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_rfl⟩
        simp_all
      · simp +contextual
    refine (nhds_basis_Ioo' hl hu).to_hasBasis' ?_ ?_
    · simp only [id_eq, and_imp, Prod.forall]
      exact fun _ _ h₁ h₂ ↦ ⟨_, by simp [h₁, h₂, Ioo_mem_nhds, convex_Ioo], subset_rfl⟩
    · simp +contextual

Похожие утверждения