AbsConvexOpenSets — Mathlib

English

The type of absolutely convex open neighborhoods of 0 in a locally convex space, equipped with a suitable 𝕜-structure.

Русский

Тип открытых абсолютно выпуклых окрестностей нуля в локально выпуклом пространстве с заданной структурой 𝕜.

LaTeX

$$$\\text{AbsConvexOpenSets}_{\\mathbb{K}}(E) = \\{ s : \\mathcal{P}(E) \\;|\\; 0 \\in s \\land IsOpen(s) \\land AbsConvex 𝕜 s\\}$$$

Lean4

/-- The type of absolutely convex open sets. -/
def AbsConvexOpenSets :=
  { s : Set E // (0 : E) ∈ s ∧ IsOpen s ∧ AbsConvex 𝕜 s }

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