Theorems · Theorem · general topology
closure_Ioo
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a b : α},
a ≠ b → closure (Set.Ioo a b) = Set.Icc a bThe closure of the open interval (a, b) is the closed interval [a, b].
- Defined in
- Mathlib.Topology.Order.DenselyOrdered
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites24
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
- TopologicalSpacestatement and proof · cited by 24,529
- LinearOrderstatement and proof · cited by 8,572
- Set.Nonemptyproof · cited by 2,627
- LT.lt.leproof · cited by 2,189
- Set.Iccstatement · cited by 1,702
- OrderTopologystatement and proof · cited by 1,355
- closurestatement and proof · cited by 1,254
- Set.Ioostatement and proof · cited by 1,214
- DenselyOrderedstatement and proof · cited by 471
- Set.Subset.antisymmproof · cited by 213
- Ne.lt_or_gtproof · cited by 108
Cited by20
Results whose statement or proof uses this declaration.
- Real.sin_nonneg_of_mem_Iccproof · cited by 6
- closure_Iocproof · cited by 5
- closure_Icoproof · cited by 4
- PhragmenLindelof.horizontal_stripproof · cited by 3
- closure_uIooproof · cited by 2
- Ioc_subset_closure_interiorproof · cited by 2
- segment_subset_closure_openSegmentproof · cited by 2
- continuousOn_Icc_extendFrom_Iooproof · cited by 2
- frontier_Iooproof · cited by 1
- closure_interior_Iccproof · cited by 1
- hasDerivWithinAt_Ici_of_tendsto_derivproof · cited by 1