Theorems · Theorem · functional analysis

Convex.eventually_nhdsWithin_segment

∀ {E : Type u_1} {𝕜 : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [LocallyConvexSpace 𝕜 E] {s : Set E},
  Convex 𝕜 s →
    ∀ {x₀ : E},
      x₀ ∈ s →
        ∀ {p : E → Prop},
          (∀ᶠ (x : E) in nhdsWithin x₀ s, p x) → ∀ᶠ (x : E) in nhdsWithin x₀ s, ∀ y ∈ segment 𝕜 x₀ x, p y

Defined in

Mathlib.Topology.Algebra.Module.LocallyConvex

Cited by

1 results in Mathlib

Foundations

Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringPartialOrderAddCommMonoidModuleTopologicalSpaceLocallyConvexSpace