Theorems · Theorem · general topology
isOpen_Ioo
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] {a b : α},
IsOpen (Set.Ioo a b)- Defined in
- Mathlib.Topology.Order.OrderClosed
- Cited by
- 54 results in Mathlib
- Foundations
- Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
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
- IsOpenstatement · cited by 2,400
- Set.Ioostatement · cited by 1,214
- OrderClosedTopologystatement and proof · cited by 445
- IsOpen.interproof · cited by 98
- isOpen_Ioiproof · cited by 43
- isOpen_Iioproof · cited by 38
Cited by54
Results whose statement or proof uses this declaration.
- measurableSet_Iooproof · cited by 42
- Ioo_mem_nhdsproof · cited by 27
- Set.OrdConnected.strictConvexproof · cited by 9
- exists_deriv_eq_slopeproof · cited by 6
- Dense.exists_betweenproof · cited by 5
- MonotoneOn.convexOn_of_derivproof · cited by 4
- uniqueDiffOn_Iooproof · cited by 4
- continuousWithinAt_right_of_monotoneOn_of_closure_image_mem_nhdsWithinproof · cited by 4
- ProbabilityTheory.IsGaussian.memLp_idproof · cited by 4
- Set.OrdConnected.measurableSetproof · cited by 4
- Set.PairwiseDisjoint.countable_of_Iooproof · cited by 4
- StrictMonoOn.strictConvexOn_of_derivproof · cited by 4