Theorems · Theorem · functional analysis
exists_enorm_lt
∀ (E : Type u_8) [inst : TopologicalSpace E] [inst_1 : ESeminormedAddMonoid E] [hbot : (nhdsWithin 0 {0}ᶜ).NeBot]
{c : ENNReal}, c ≠ 0 → ∃ x, x ≠ 0 ∧ ‖x‖ₑ < c- Defined in
- Mathlib.Analysis.Normed.Group.Basic
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 128 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites16
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- ENNRealstatement and proof · cited by 9,879
- Compl.complstatement and proof · cited by 2,925
- nhdsWithinstatement and proof · cited by 1,912
- Filter.NeBotstatement and proof · cited by 853
- ENorm.enormstatement · cited by 715
- ESeminormedAddMonoidstatement and proof · cited by 133
- Ne.bot_ltproof · cited by 116
- Continuous.tendsto'proof · cited by 53
- Filter.Frequently.and_eventuallyproof · cited by 49
- enorm_zeroproof · cited by 44
Cited by1
Results whose statement or proof uses this declaration.
- egauge_pi'proof · cited by 2