Theorems · Theorem · general topology
CompactIccSpace.isCompact_Icc
∀ {α : Type u_1} {inst : TopologicalSpace α} {inst_1 : Preorder α} [self : CompactIccSpace α] {a b : α},
IsCompact (Set.Icc a b)A closed interval Set.Icc a b is a compact set for all a and b.
- Defined in
- Mathlib.Topology.Order.Compact
- Cited by
- 42 results in Mathlib
- Foundations
- Depth 50 from the axioms · uses propext, Quot.sound
- Assumes
- CompactIccSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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
- Preorderstatement and proof · cited by 7,952
- Set.Iccstatement · cited by 1,702
- IsCompactstatement · cited by 1,282
- CompactIccSpacestatement and proof · cited by 96
Cited by42
Results whose statement or proof uses this declaration.
- isCompact_uIccproof · cited by 17
- ContinuousOn.integrableOn_Iccproof · cited by 8
- BoxIntegral.Box.isCompact_Iccproof · cited by 7
- measure_Icc_lt_topproof · cited by 5
- totallyBounded_Iccproof · cited by 5
- MeasureTheory.integrableOn_Iic_iff_integrableAtFilter_atBotproof · cited by 3
- isCompact_setOfPred_finiteMeasure_le_of_compactSpaceproof · cited by 3
- NumberField.mixedEmbedding.fundamentalCone.isCompact_compactSetproof · cited by 3
- exists_Ioo_extr_on_Iccproof · cited by 3
- IsAddFoelner.tendsto_nhds_meanproof · cited by 3
- cocompact_le_atBotproof · cited by 3
- IsFoelner.tendsto_nhds_meanproof · cited by 3