Theorems · Theorem · functional analysis
isBounded_iff_forall_norm_le
∀ {E : Type u_2} [inst : SeminormedAddGroup E] {s : Set E}, Bornology.IsBounded s ↔ ∃ C, ∀ x ∈ s, ‖x‖ ≤ C- Defined in
- Mathlib.Analysis.Normed.Group.Bounded
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 105 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- SeminormedAddGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Realstatement and proof · cited by 25,697
- Norm.normstatement · cited by 5,413
- SeminormedAddGroupstatement and proof · cited by 331
- Bornology.IsBoundedstatement and proof · cited by 293
- mem_closedBall_zero_iffproof · cited by 16
- Metric.isBounded_iff_subset_closedBallproof · cited by 10
Cited by17
Results whose statement or proof uses this declaration.
- IsCompact.exists_bound_of_continuousOnproof · cited by 8
- Bornology.IsBounded.exists_norm_leproof · cited by 6
- ConvexOn.continuousOn_tfaeproof · cited by 3
- NormedSpace.unbounded_univproof · cited by 3
- ZSpan.fundamentalDomain_isBoundedproof · cited by 3
- MonotoneOn.memLp_topproof · cited by 2
- Bornology.IsBounded.addproof · cited by 2
- BoundedContinuousFunction.isBounded_range_integralproof · cited by 2
- Bornology.IsBounded.negproof · cited by 2
- NormedSpace.isVonNBounded_iff'proof · cited by 1
- Complex.liouville_theorem_auxproof · cited by 1
- NumberField.mixedEmbedding.fundamentalCone.isBounded_normLeOneproof · cited by 1