Theorems · Theorem · functional analysis

egauge_eq_zero_iff

∀ {𝕜 : Type u_1} [inst : NormedDivisionRing 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {s : Set E} {x : E}, egauge 𝕜 s x = 0 ↔ ∃ᶠ (c : 𝕜) in nhds 0, x ∈ c • s

Defined in

Mathlib.Analysis.Convex.EGauge

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedDivisionRingAddCommGroupModule