Theorems · Theorem · convex and discrete geometry

Convex.nhdsWithin_sdiff_eq_nhdsLT

∀ {𝕜 : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [OrderTopology 𝕜] {s : Set 𝕜},
  Convex 𝕜 s →
    ∀ {a : 𝕜},
      a ∈ closure s → (s ∩ Set.Iio a).Nonempty → s ∩ Set.Ioi a = ∅ → nhdsWithin a (s \ {a}) = nhdsWithin a (Set.Iio a)

Defined in

Mathlib.Analysis.Convex.Topology

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldLinearOrderIsStrictOrderedRingTopologicalSpaceOrderTopology