Theorems · Theorem · functional analysis
IsCompact.exists_bound_of_continuousOn
∀ {α : Type u_1} {E : Type u_2} [inst : SeminormedAddGroup E] [inst_1 : TopologicalSpace α] {s : Set α},
IsCompact s → ∀ {f : α → E}, ContinuousOn f s → ∃ C, ∀ x ∈ s, ‖f x‖ ≤ C- Defined in
- Mathlib.Analysis.Normed.Group.Bounded
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 117 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
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
- TopologicalSpacestatement and proof · cited by 24,529
- Set.imageproof · cited by 5,609
- Norm.normstatement and proof · cited by 5,413
- ContinuousOnstatement and proof · cited by 1,411
- IsCompactstatement and proof · cited by 1,282
- Set.mem_image_of_memproof · cited by 371
- SeminormedAddGroupstatement and proof · cited by 331
- IsCompact.isBoundedproof · cited by 29
- IsCompact.image_of_continuousOnproof · cited by 24
- isBounded_iff_forall_norm_leproof · cited by 17
Cited by8
Results whose statement or proof uses this declaration.
- MeasureTheory.IntegrableOn.mul_continuousOn_of_subsetproof · cited by 2
- MeasureTheory.IntegrableOn.continuousOn_mul_of_subsetproof · cited by 2
- MeasureTheory.IntegrableOn.continuousOn_smul_of_subsetproof · cited by 2
- continuousOn_integral_bilinear_of_locally_integrable_of_compact_supportproof · cited by 2
- MeasureTheory.IntegrableOn.smul_continuousOn_of_subsetproof · cited by 2
- AbsolutelyContinuousOnInterval.exists_boundproof · cited by 1
- tendsto_tsum_div_pow_atTop_integralproof · cited by 1
- ModularGroup.exists_bound_fundamental_domain_of_isBigOproof · cited by 1