Theorems · Theorem · general topology
IsPreconnected.eq_univ_of_unbounded
∀ {α : Type v} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {s : Set α},
IsPreconnected s → ¬BddBelow s → ¬BddAbove s → s = Set.univIf a preconnected set in a linear order space is unbounded below and above, then it is the whole space.
- Defined in
- Mathlib.Topology.Order.IntermediateValue
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
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.univstatement · cited by 3,945
- le_of_ltproof · cited by 1,175
- BddAbovestatement and proof · cited by 620
- OrderClosedTopologystatement and proof · cited by 445
- BddBelowstatement and proof · cited by 401
- IsPreconnectedstatement and proof · cited by 205
- Set.eq_univ_of_forallproof · cited by 80
- not_bddAbove_iffproof · cited by 15
- not_bddBelow_iffproof · cited by 5
Cited by1
Results whose statement or proof uses this declaration.
- IsPreconnected.mem_intervalsproof · cited by 1