Theorems · Theorem · field theory
NormedField.exists_lt_norm
∀ (α : Type u_2) [inst : NontriviallyNormedField α] (r : ℝ), ∃ x, r < ‖x‖
- Defined in
- Mathlib.Analysis.Normed.Field.Basic
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 117 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- NontriviallyNormedField
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- NontriviallyNormedFieldstatement and proof · cited by 8,742
- Norm.normstatement and proof · cited by 5,413
- norm_powproof · cited by 106
- NormedField.exists_one_lt_normproof · cited by 19
- pow_unbounded_of_one_ltproof · cited by 7
Cited by14
Results whose statement or proof uses this declaration.
- NormedField.exists_norm_ltproof · cited by 11
- NormedSpace.isVonNBounded_iffproof · cited by 9
- IsCompactOperator.image_subset_compact_of_isVonNBoundedproof · cited by 4
- NormedSpace.exists_lt_normproof · cited by 2
- WithSeminorms.isVonNBounded_iff_finset_seminorm_boundedproof · cited by 2
- NormedField.exists_lt_nnnormproof · cited by 2
- LinearMap.polar_subMulActionproof · cited by 1
- cardinal_eq_of_mem_nhds_zeroproof · cited by 1
- NormedSpace.isBounded_iff_subset_smul_ballproof · cited by 1
- mem_tangentConeAt_iff_exists_seq_norm_tendsto_atTopproof · cited by 0
- NormedField.completeSpace_iff_isComplete_closedBallproof · cited by 0
- NormedField.discreteTopology_of_bddAbove_range_normproof · cited by 0