Theorems · Theorem · general topology
isCompact_uIcc
∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [CompactIccSpace α] {a b : α},
IsCompact (Set.uIcc a b)An unordered closed interval is compact.
- Defined in
- Mathlib.Topology.Order.Compact
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 51 from the axioms · uses propext, Quot.sound
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.
- TopologicalSpacestatement and proof · cited by 24,529
- LinearOrderstatement and proof · cited by 8,572
- IsCompactstatement · cited by 1,282
- Set.uIccstatement · cited by 393
- CompactIccSpacestatement and proof · cited by 96
- CompactIccSpace.isCompact_Iccproof · cited by 42
Cited by17
Results whose statement or proof uses this declaration.
- IntervalIntegrable.continuousOn_mulproof · cited by 8
- IntervalIntegrable.mul_continuousOnproof · cited by 7
- IntervalIntegrable.continuousOn_smulproof · cited by 6
- MonotoneOn.intervalIntegrableproof · cited by 4
- MeromorphicOn.intervalIntegrable_log_normproof · cited by 4
- IntervalIntegrable.smul_continuousOnproof · cited by 3
- Frullani.intervalIntegrable_inv_smulproof · cited by 2
- exists_eq_interval_average_of_nullSingletonClassproof · cited by 2
- TendstoUniformlyOn.tendsto_intervalIntegral_of_continuousOnproof · cited by 1
- intervalIntegral.tsum_intervalIntegral_eq_of_summable_normstatement and proof · cited by 1
- LocallyIntegrable.ae_hasDerivAt_integralproof · cited by 1
- Function.Periodic.compact_of_continuousproof · cited by 1