Theorems · Theorem · order theory
Set.ordConnected_iff_disjoint_Ioo_empty
∀ {α : Type u_1} {I : Set α} [inst : LinearOrder α] [LocallyFiniteOrder α],
I.OrdConnected ↔ ∀ x ∈ I, ∀ y ∈ I, Disjoint (Set.Ioo x y) I → Set.Ioo x y = ∅- Cited by
- 0 results in Mathlib
- Foundations
- Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites31
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
- LinearOrderstatement and proof · cited by 8,572
- Compl.complproof · cited by 2,925
- Set.extproof · cited by 2,266
- Disjointstatement · cited by 2,201
- LT.lt.leproof · cited by 2,189
- le_reflproof · cited by 2,061
- Set.Iccproof · cited by 1,702
- Set.Ioostatement and proof · cited by 1,214
- le_transproof · cited by 985
- Set.Iocproof · cited by 971
- Set.Icoproof · cited by 799
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.