IntermediateValue

📁 Source: Mathlib/Topology/Order/IntermediateValue.lean

Statistics

Metric	Count
Definitions	0
Theorems `strictAnti_of_inj_boundedOrder`, `strictMonoOn_of_inj_rigidity`, `strictMono_of_inj`, `strictMono_of_inj_boundedOrder`, `strictMono_of_inj_boundedOrder'`, `surjective`, `surjective'`, `strictAntiOn_of_injOn_Icc`, `strictMonoOn_of_injOn_Icc`, `strictMonoOn_of_injOn_Icc'`, `strictMonoOn_of_injOn_Ioo`, `surjOn_Icc`, `surjOn_of_tendsto`, `surjOn_of_tendsto'`, `surjOn_uIcc`, `Icc_subset_of_forall_exists_gt`, `Icc_subset_of_forall_exists_lt`, `Icc_subset_of_forall_mem_nhdsGT_of_Icc_subset`, `Icc_subset_of_forall_mem_nhdsWithin`, `mem_of_ge_of_forall_exists_gt`, `mem_of_ge_of_forall_exists_lt`, `Icc_subset`, `Ioo_csInf_csSup_subset`, `Icc_subset`, `Iio_csSup_subset`, `Ioi_csInf_subset`, `eq_univ_of_unbounded`, `intermediate_value`, `intermediate_value_Ici`, `intermediate_value_Ico`, `intermediate_value_Iic`, `intermediate_value_Iii`, `intermediate_value_Iio`, `intermediate_value_Ioc`, `intermediate_value_Ioi`, `intermediate_value_Ioo`, `intermediate_value₂`, `intermediate_value₂_eventually₁`, `intermediate_value₂_eventually₂`, `mem_intervals`, `ordConnected`, `isPreconnected`, `eq_Icc_csInf_csSup_of_connected_bdd_closed`, `exists_mem_Icc_isFixedPt`, `exists_mem_Icc_isFixedPt_of_mapsTo`, `exists_mem_uIcc_isFixedPt`, `intermediate_value_Icc`, `intermediate_value_Icc'`, `intermediate_value_Ico`, `intermediate_value_Ico'`, `intermediate_value_Ioc`, `intermediate_value_Ioc'`, `intermediate_value_Ioo`, `intermediate_value_Ioo'`, `intermediate_value_uIcc`, `intermediate_value_univ`, `intermediate_value_univ₂`, `intermediate_value_univ₂_eventually₁`, `intermediate_value_univ₂_eventually₂`, `isConnected_Icc`, `isConnected_Ici`, `isConnected_Ico`, `isConnected_Iic`, `isConnected_Iio`, `isConnected_Ioc`, `isConnected_Ioi`, `isConnected_Ioo`, `isConnected_uIoc`, `isConnected_uIoo`, `isPreconnected_Icc`, `isPreconnected_Icc_aux`, `isPreconnected_Ici`, `isPreconnected_Ico`, `isPreconnected_Iic`, `isPreconnected_Iio`, `isPreconnected_Ioc`, `isPreconnected_Ioi`, `isPreconnected_Ioo`, `isPreconnected_iff_ordConnected`, `isPreconnected_uIcc`, `isPreconnected_uIoc`, `isPreconnected_uIoo`, `isTotallyDisconnected_iff_lt`, `mem_range_of_exists_le_of_exists_ge`, `ordered_connected_space`, `setOf_isPreconnected_eq_of_ordered`, `setOf_isPreconnected_subset_of_ordered`	87
Total	87

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`strictAnti_of_inj_boundedOrder` 📖	mathematical	`Continuous` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Top.top` `OrderTop.toTop` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `BoundedOrder.toOrderTop` `Bot.bot` `OrderBot.toBot` `BoundedOrder.toOrderBot`	`StrictAnti` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`strictMono_of_inj_boundedOrder` `instOrderClosedTopologyOrderDual`
`strictMonoOn_of_inj_rigidity` 📖	mathematical	`Continuous` `Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `StrictMonoOn` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Icc`	`StrictMono` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`min_le_left` `le_max_left` `LE.le.trans` `LE.le.trans'` `LT.lt.le` `strictMono_of_inj_boundedOrder'` `orderTopology_of_ordConnected` `Set.ordConnected_Icc` `Set.instDenselyOrdered` `ContinuousOn.restrict` `continuousOn` `Set.InjOn.injective` `Function.Injective.injOn` `strictMono_restrict` `Set.strictAntiOn_iff_strictAnti` `Set.Icc_subset_Icc` `StrictAntiOn.mono` `IsAntichain.of_strictMonoOn_antitoneOn` `StrictAntiOn.antitoneOn` `IsAntichain.not_lt` `Set.left_mem_Icc` `le_of_lt` `Set.right_mem_Icc` `min_le_right` `le_max_right` `StrictMonoOn.mono`
`strictMono_of_inj` 📖	mathematical	`Continuous`	`StrictMono` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `StrictAnti`	—	`strictMonoOn_of_inj_rigidity` `instOrderClosedTopologyOrderDual` `ContinuousOn.strictMonoOn_of_injOn_Icc'` `LT.lt.le` `continuousOn` `Function.Injective.injOn` `subsingleton_or_nontrivial` `Subsingleton.strictMono` `exists_pair_lt`
`strictMono_of_inj_boundedOrder` 📖	mathematical	`Continuous` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Bot.bot` `OrderBot.toBot` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `BoundedOrder.toOrderBot` `Top.top` `OrderTop.toTop` `BoundedOrder.toOrderTop`	`StrictMono` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`lt_of_le_of_ne` `LT.lt.ne'` `intermediate_value_Ioc` `le_top` `continuousOn` `LT.lt.trans_le` `Set.Ioc_top` `intermediate_value_Ioo` `bot_le` `LT.lt.false` `LT.lt.trans` `lt_of_lt_of_le'` `intermediate_value_Ioo'` `LT.lt.le`
`strictMono_of_inj_boundedOrder'` 📖	mathematical	`Continuous`	`StrictMono` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `StrictAnti`	—	`strictMono_of_inj_boundedOrder` `strictAnti_of_inj_boundedOrder` `le_total`
`surjective` 📖	—	`Continuous` `Filter.Tendsto` `Filter.atTop` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Filter.atBot`	—	—	`mem_range_of_exists_le_of_exists_ge` `ordered_connected_space` `Filter.Eventually.exists` `Filter.atBot_neBot` `SemilatticeInf.instIsCodirectedOrder` `supSet_to_nonempty` `Filter.Tendsto.eventually` `Filter.eventually_le_atBot` `Filter.atTop_neBot` `SemilatticeSup.instIsDirectedOrder` `Filter.eventually_ge_atTop`
`surjective'` 📖	—	`Continuous` `Filter.Tendsto` `Filter.atBot` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Filter.atTop` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	—	`surjective` `instOrderTopologyOrderDual` `OrderDual.denselyOrdered`

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`strictAntiOn_of_injOn_Icc` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ContinuousOn` `Set.Icc` `Set.InjOn`	`StrictAntiOn` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Icc`	—	`strictMonoOn_of_injOn_Icc` `instOrderClosedTopologyOrderDual`
`strictMonoOn_of_injOn_Icc` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ContinuousOn` `Set.Icc` `Set.InjOn`	`StrictMonoOn` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Icc`	—	`StrictMono.of_restrict` `Continuous.strictMono_of_inj_boundedOrder` `orderTopology_of_ordConnected` `Set.ordConnected_Icc` `Set.instDenselyOrdered` `restrict` `Set.InjOn.injective`
`strictMonoOn_of_injOn_Icc'` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ContinuousOn` `Set.Icc` `Set.InjOn`	`StrictMonoOn` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Icc` `StrictAntiOn`	—	`strictMonoOn_of_injOn_Icc` `strictAntiOn_of_injOn_Icc` `le_total`
`strictMonoOn_of_injOn_Ioo` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ContinuousOn` `Set.Ioo` `Set.InjOn`	`StrictMonoOn` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ioo` `StrictAntiOn`	—	`Set.nonempty_Ioo_subtype` `Set.ordConnected_Ioo` `orderTopology_of_ordConnected` `Set.instDenselyOrdered` `restrict` `Set.InjOn.injective` `strictMono_restrict` `Set.strictAntiOn_iff_strictAnti`
`surjOn_Icc` 📖	mathematical	`ContinuousOn` `Set` `Set.instMembership`	`Set.SurjOn` `Set.Icc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`IsPreconnected.intermediate_value` `Set.OrdConnected.isPreconnected`
`surjOn_of_tendsto` 📖	mathematical	`Set.Nonempty` `ContinuousOn` `Filter.Tendsto` `Set.Elem` `Set` `Set.instMembership` `Filter.atBot` `Subtype.preorder` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Filter.atTop`	`Set.SurjOn` `Set.univ`	—	`Set.surjOn_iff_surjective` `Continuous.surjective` `Set.Nonempty.to_subtype` `orderTopology_of_ordConnected` `Set.instDenselyOrdered` `restrict`
`surjOn_of_tendsto'` 📖	mathematical	`Set.Nonempty` `ContinuousOn` `Filter.Tendsto` `Set.Elem` `Set` `Set.instMembership` `Filter.atBot` `Subtype.preorder` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Filter.atTop` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Set.SurjOn` `Set.univ`	—	`surjOn_of_tendsto` `instOrderClosedTopologyOrderDual`
`surjOn_uIcc` 📖	mathematical	`ContinuousOn` `Set` `Set.instMembership`	`Set.SurjOn` `Set.uIcc` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`le_total` `Set.uIcc_of_le` `surjOn_Icc` `Set.uIcc_of_ge`

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Icc_subset_of_forall_exists_gt` 📖	mathematical	`Set` `Set.instMembership` `Set.Nonempty` `Set.instInter` `Set.Ioc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`Set` `Set.instHasSubset` `Set.Icc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`inter` `isClosed_Icc` `OrderTopology.to_orderClosedTopology` `mem_of_ge_of_forall_exists_gt` `Set.Ico_subset_Ico_right`
`Icc_subset_of_forall_exists_lt` 📖	mathematical	`Set` `Set.instMembership` `Set.Nonempty` `Set.instInter` `Set.Ico` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`Set` `Set.instHasSubset` `Set.Icc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`inter` `isClosed_Icc` `OrderTopology.to_orderClosedTopology` `mem_of_ge_of_forall_exists_lt` `Set.Ioc_subset_Ioc_left`
`Icc_subset_of_forall_mem_nhdsGT_of_Icc_subset` 📖	mathematical	`Set` `Set.instMembership` `Filter` `Filter.instMembership` `nhdsWithin` `Set.Ioi` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`Set` `Set.instHasSubset` `Set.Icc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`lt_or_ge` `Set.Icc_eq_empty` `Set.left_mem_Icc` `Set.Icc_self` `le_csSup` `csSup_le` `LE.le.eq_or_lt` `closure_subset_iff` `le_rfl` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.inter_subset_left` `csSup_mem_closure` `lt_csSup_iff` `LT.lt.le` `eq_of_le_of_not_lt` `mem_nhdsGT_iff_exists_Ioo_subset'` `exists_between` `lt_min` `ne_of_lt` `le_antisymm` `le_trans` `le_of_lt` `le_refl` `LE.le.trans` `min_le_right` `le_or_gt` `LE.le.trans_lt` `LT.lt.trans_le` `min_le_left`
`Icc_subset_of_forall_mem_nhdsWithin` 📖	mathematical	`Set` `Set.instMembership` `Filter` `Filter.instMembership` `nhdsWithin` `Set.Ioi` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`Set` `Set.instHasSubset` `Set.Icc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`Icc_subset_of_forall_mem_nhdsGT_of_Icc_subset` `le_rfl`
`mem_of_ge_of_forall_exists_gt` 📖	mathematical	`Set` `Set.instMembership` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Set.Nonempty` `Set.instInter` `Set.Ioc`	`Set` `Set.instMembership`	—	`Set.left_mem_Icc` `csSup_mem` `csSup_le` `eq_or_lt_of_le` `not_lt_of_ge` `le_csSup` `le_trans` `le_of_lt`
`mem_of_ge_of_forall_exists_lt` 📖	mathematical	`Set` `Set.instMembership` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Set.Nonempty` `Set.instInter` `Set.Ico`	`Set` `Set.instMembership`	—	`mem_of_ge_of_forall_exists_gt` `instOrderTopologyOrderDual` `Set.Icc_toDual` `Set.preimage_inter` `Set.mem_image` `Equiv.image_symm_eq_preimage` `Set.Ico_toDual` `Set.Ioc_toDual`

IsConnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Icc_subset` 📖	mathematical	`IsConnected` `Set` `Set.instMembership`	`Set` `Set.instHasSubset` `Set.Icc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`IsPreconnected.Icc_subset`
`Ioo_csInf_csSup_subset` 📖	mathematical	`IsConnected` `BddBelow` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `BddAbove`	`Set` `Set.instHasSubset` `Set.Ioo` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`isGLB_lt_iff` `isGLB_csInf` `nonempty` `lt_isLUB_iff` `isLUB_csSup` `Icc_subset` `OrderTopology.to_orderClosedTopology` `LT.lt.le`

IsPreconnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Icc_subset` 📖	mathematical	`IsPreconnected` `Set` `Set.instMembership`	`Set` `Set.instHasSubset` `Set.Icc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Set.image_id` `intermediate_value` `continuousOn_id`
`Iio_csSup_subset` 📖	mathematical	`IsPreconnected` `BddBelow` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `BddAbove`	`Set` `Set.instHasSubset` `Set.Iio` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`Ioi_csInf_subset` `instOrderTopologyOrderDual`
`Ioi_csInf_subset` 📖	mathematical	`IsPreconnected` `BddBelow` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `BddAbove`	`Set` `Set.instHasSubset` `Set.Ioi` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf`	—	`nonempty_of_not_bddAbove` `supSet_to_nonempty` `isGLB_lt_iff` `isGLB_csInf` `not_bddAbove_iff` `Icc_subset` `OrderTopology.to_orderClosedTopology` `LT.lt.le`
`eq_univ_of_unbounded` 📖	mathematical	`IsPreconnected` `BddBelow` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `BddAbove`	`Set.univ`	—	`Set.eq_univ_of_forall` `not_bddBelow_iff` `not_bddAbove_iff` `Icc_subset` `le_of_lt`
`intermediate_value` 📖	mathematical	`IsPreconnected` `Set` `Set.instMembership` `ContinuousOn`	`Set` `Set.instHasSubset` `Set.Icc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.image`	—	`intermediate_value₂` `continuousOn_const`
`intermediate_value_Ici` 📖	mathematical	`IsPreconnected` `Set` `Set.instMembership` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.principal` `ContinuousOn` `Filter.Tendsto` `Filter.atTop` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Set` `Set.instHasSubset` `Set.Ici` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.image`	—	`intermediate_value₂_eventually₁` `continuousOn_const` `Filter.tendsto_atTop`
`intermediate_value_Ico` 📖	mathematical	`IsPreconnected` `Set` `Set.instMembership` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.principal` `ContinuousOn` `Filter.Tendsto` `nhds`	`Set` `Set.instHasSubset` `Set.Ico` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.image`	—	`intermediate_value₂_eventually₁` `continuousOn_const` `Filter.Tendsto.eventually_const_le` `instClosedIicTopology`
`intermediate_value_Iic` 📖	mathematical	`IsPreconnected` `Set` `Set.instMembership` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.principal` `ContinuousOn` `Filter.Tendsto` `Filter.atBot` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Set` `Set.instHasSubset` `Set.Iic` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.image`	—	`intermediate_value₂_eventually₁` `continuousOn_const` `Filter.tendsto_atBot`
`intermediate_value_Iii` 📖	mathematical	`IsPreconnected` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.principal` `ContinuousOn` `Filter.Tendsto` `Filter.atBot` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Filter.atTop`	`Set` `Set.instHasSubset` `Set.univ` `Set.image`	—	`intermediate_value₂_eventually₂` `continuousOn_const` `Filter.Tendsto.eventually_le_atBot` `Filter.Tendsto.eventually_ge_atTop`
`intermediate_value_Iio` 📖	mathematical	`IsPreconnected` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.principal` `ContinuousOn` `Filter.Tendsto` `Filter.atBot` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `nhds`	`Set` `Set.instHasSubset` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.image`	—	`intermediate_value₂_eventually₂` `continuousOn_const` `Filter.Tendsto.eventually_le_atBot` `Filter.Tendsto.eventually_const_le` `instClosedIicTopology`
`intermediate_value_Ioc` 📖	mathematical	`IsPreconnected` `Set` `Set.instMembership` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.principal` `ContinuousOn` `Filter.Tendsto` `nhds`	`Set` `Set.instHasSubset` `Set.Ioc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.image`	—	`intermediate_value₂_eventually₁` `continuousOn_const` `Filter.Tendsto.eventually_le_const` `instClosedIciTopology`
`intermediate_value_Ioi` 📖	mathematical	`IsPreconnected` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.principal` `ContinuousOn` `Filter.Tendsto` `nhds` `Filter.atTop` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Set` `Set.instHasSubset` `Set.Ioi` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.image`	—	`intermediate_value₂_eventually₂` `continuousOn_const` `Filter.Tendsto.eventually_le_const` `instClosedIciTopology` `Filter.Tendsto.eventually_ge_atTop`
`intermediate_value_Ioo` 📖	mathematical	`IsPreconnected` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.principal` `ContinuousOn` `Filter.Tendsto` `nhds`	`Set` `Set.instHasSubset` `Set.Ioo` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.image`	—	`intermediate_value₂_eventually₂` `continuousOn_const` `Filter.Tendsto.eventually_le_const` `instClosedIciTopology` `Filter.Tendsto.eventually_const_le` `instClosedIicTopology`
`intermediate_value₂` 📖	mathematical	`IsPreconnected` `Set` `Set.instMembership` `ContinuousOn` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Set` `Set.instMembership`	—	`intermediate_value_univ₂` `Subtype.preconnectedSpace` `continuousOn_iff_continuous_restrict`
`intermediate_value₂_eventually₁` 📖	mathematical	`IsPreconnected` `Set` `Set.instMembership` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.principal` `ContinuousOn` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Filter.EventuallyLE`	`Set` `Set.instMembership`	—	`intermediate_value_univ₂_eventually₁` `Subtype.preconnectedSpace` `Filter.comap_coe_neBot_of_le_principal` `continuousOn_iff_continuous_restrict` `Filter.Eventually.comap` `Subtype.prop`
`intermediate_value₂_eventually₂` 📖	mathematical	`IsPreconnected` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.principal` `ContinuousOn` `Filter.EventuallyLE` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Set` `Set.instMembership`	—	`intermediate_value_univ₂_eventually₂` `Subtype.preconnectedSpace` `Filter.comap_coe_neBot_of_le_principal` `continuousOn_iff_continuous_restrict` `Filter.Eventually.comap` `Subtype.prop`
`mem_intervals` 📖	mathematical	`IsPreconnected`	`Set` `Set.instMembership` `Set.instInsert` `Set.Icc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `Set.Ico` `Set.Ioc` `Set.Ioo` `Set.Ici` `Set.Ioi` `Set.Iic` `Set.Iio` `Set.univ` `Set.instSingletonSet` `Set.instEmptyCollection`	—	`Set.eq_empty_or_nonempty` `Set.mem_singleton` `Set.mem_of_subset_of_mem` `Set.mem_Icc_Ico_Ioc_Ioo_of_subset_of_subset` `IsConnected.Ioo_csInf_csSup_subset` `subset_Icc_csInf_csSup` `Set.mem_Ici_Ioi_of_subset_of_subset` `Ioi_csInf_subset` `csInf_le` `Set.mem_Iic_Iio_of_subset_of_subset` `Iio_csSup_subset` `le_csSup` `eq_univ_of_unbounded` `OrderTopology.to_orderClosedTopology`
`ordConnected` 📖	mathematical	`IsPreconnected`	`Set.OrdConnected` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Icc_subset`

Set.OrdConnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPreconnected` 📖	mathematical	—	`IsPreconnected`	—	`isPreconnected_of_forall_pair` `uIcc_subset` `Set.left_mem_uIcc` `Set.right_mem_uIcc` `isPreconnected_uIcc`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_Icc_csInf_csSup_of_connected_bdd_closed` 📖	mathematical	`IsConnected` `BddBelow` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `BddAbove`	`Set.Icc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `subset_Icc_csInf_csSup` `IsConnected.Icc_subset` `OrderTopology.to_orderClosedTopology` `IsClosed.csInf_mem` `IsConnected.nonempty` `IsClosed.csSup_mem`
`exists_mem_Icc_isFixedPt` 📖	mathematical	`ContinuousOn` `Set.Icc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Preorder.toLE`	`Set` `Set.instMembership` `Set.Icc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Function.IsFixedPt`	—	`IsPreconnected.intermediate_value₂` `OrderTopology.to_orderClosedTopology` `isPreconnected_Icc` `Set.right_mem_Icc` `Set.left_mem_Icc` `continuousOn_id`
`exists_mem_Icc_isFixedPt_of_mapsTo` 📖	mathematical	`ContinuousOn` `Set.Icc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Preorder.toLE` `Set.MapsTo`	`Set` `Set.instMembership` `Set.Icc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Function.IsFixedPt`	—	`exists_mem_Icc_isFixedPt` `Set.left_mem_Icc` `Set.right_mem_Icc`
`exists_mem_uIcc_isFixedPt` 📖	mathematical	`ContinuousOn` `Set.uIcc` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder`	`Set` `Set.instMembership` `Set.uIcc` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Function.IsFixedPt`	—	`IsPreconnected.intermediate_value₂` `OrderTopology.to_orderClosedTopology` `isPreconnected_uIcc` `Set.right_mem_uIcc` `Set.left_mem_uIcc` `continuousOn_id`
`intermediate_value_Icc` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ContinuousOn` `Set.Icc`	`Set` `Set.instHasSubset` `Set.Icc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.image` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`IsPreconnected.intermediate_value` `isPreconnected_Icc` `Set.left_mem_Icc` `Set.right_mem_Icc`
`intermediate_value_Icc'` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ContinuousOn` `Set.Icc`	`Set` `Set.instHasSubset` `Set.Icc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.image` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`IsPreconnected.intermediate_value` `isPreconnected_Icc` `Set.right_mem_Icc` `Set.left_mem_Icc`
`intermediate_value_Ico` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ContinuousOn` `Set.Icc`	`Set` `Set.instHasSubset` `Set.Ico` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.image` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`eq_or_lt_of_le` `not_lt_of_ge` `IsPreconnected.intermediate_value_Ico` `isPreconnected_Ico` `refl` `instReflLe` `right_nhdsWithin_Ico_neBot` `inf_le_right` `ContinuousOn.mono` `Set.Ico_subset_Icc_self` `ContinuousWithinAt.mono` `ContinuousOn.continuousWithinAt`
`intermediate_value_Ico'` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ContinuousOn` `Set.Icc`	`Set` `Set.instHasSubset` `Set.Ioc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.image` `Set.Ico` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`eq_or_lt_of_le` `not_lt_of_ge` `IsPreconnected.intermediate_value_Ioc` `isPreconnected_Ico` `refl` `instReflLe` `right_nhdsWithin_Ico_neBot` `inf_le_right` `ContinuousOn.mono` `Set.Ico_subset_Icc_self` `ContinuousWithinAt.mono` `ContinuousOn.continuousWithinAt`
`intermediate_value_Ioc` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ContinuousOn` `Set.Icc`	`Set` `Set.instHasSubset` `Set.Ioc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.image` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`eq_or_lt_of_le` `not_le_of_gt` `IsPreconnected.intermediate_value_Ioc` `isPreconnected_Ioc` `refl` `instReflLe` `left_nhdsWithin_Ioc_neBot` `inf_le_right` `ContinuousOn.mono` `Set.Ioc_subset_Icc_self` `ContinuousWithinAt.mono` `ContinuousOn.continuousWithinAt`
`intermediate_value_Ioc'` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ContinuousOn` `Set.Icc`	`Set` `Set.instHasSubset` `Set.Ico` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.image` `Set.Ioc` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`eq_or_lt_of_le` `not_le_of_gt` `IsPreconnected.intermediate_value_Ico` `isPreconnected_Ioc` `refl` `instReflLe` `left_nhdsWithin_Ioc_neBot` `inf_le_right` `ContinuousOn.mono` `Set.Ioc_subset_Icc_self` `ContinuousWithinAt.mono` `ContinuousOn.continuousWithinAt`
`intermediate_value_Ioo` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ContinuousOn` `Set.Icc`	`Set` `Set.instHasSubset` `Set.Ioo` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.image` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`eq_or_lt_of_le` `not_lt_of_gt` `IsPreconnected.intermediate_value_Ioo` `isPreconnected_Ioo` `left_nhdsWithin_Ioo_neBot` `right_nhdsWithin_Ioo_neBot` `inf_le_right` `ContinuousOn.mono` `Set.Ioo_subset_Icc_self` `ContinuousWithinAt.mono` `ContinuousOn.continuousWithinAt` `refl` `instReflLe`
`intermediate_value_Ioo'` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ContinuousOn` `Set.Icc`	`Set` `Set.instHasSubset` `Set.Ioo` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.image` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`eq_or_lt_of_le` `not_lt_of_gt` `IsPreconnected.intermediate_value_Ioo` `isPreconnected_Ioo` `right_nhdsWithin_Ioo_neBot` `left_nhdsWithin_Ioo_neBot` `inf_le_right` `ContinuousOn.mono` `Set.Ioo_subset_Icc_self` `ContinuousWithinAt.mono` `ContinuousOn.continuousWithinAt` `refl` `instReflLe`
`intermediate_value_uIcc` 📖	mathematical	`ContinuousOn` `Set.uIcc` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`Set` `Set.instHasSubset` `Set.uIcc` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.image` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`le_total` `Set.uIcc_of_le` `IsPreconnected.intermediate_value` `isPreconnected_uIcc` `Set.uIcc_of_ge`
`intermediate_value_univ` 📖	mathematical	`Continuous`	`Set` `Set.instHasSubset` `Set.Icc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.range`	—	`intermediate_value_univ₂` `continuous_const`
`intermediate_value_univ₂` 📖	—	`Continuous` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	—	`isPreconnected_closed_iff` `PreconnectedSpace.isPreconnected_univ` `isClosed_le` `le_total` `le_antisymm`
`intermediate_value_univ₂_eventually₁` 📖	—	`Continuous` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Filter.EventuallyLE`	—	—	`Filter.Eventually.exists` `intermediate_value_univ₂`
`intermediate_value_univ₂_eventually₂` 📖	—	`Continuous` `Filter.EventuallyLE` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	—	`Filter.Eventually.exists` `intermediate_value_univ₂`
`isConnected_Icc` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`IsConnected` `Set.Icc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`Set.nonempty_Icc` `isPreconnected_Icc`
`isConnected_Ici` 📖	mathematical	—	`IsConnected` `Set.Ici` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`Set.nonempty_Ici` `isPreconnected_Ici`
`isConnected_Ico` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`IsConnected` `Set.Ico` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`Set.nonempty_Ico` `isPreconnected_Ico`
`isConnected_Iic` 📖	mathematical	—	`IsConnected` `Set.Iic` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`Set.nonempty_Iic` `isPreconnected_Iic`
`isConnected_Iio` 📖	mathematical	—	`IsConnected` `Set.Iio` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`Set.nonempty_Iio` `isPreconnected_Iio`
`isConnected_Ioc` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`IsConnected` `Set.Ioc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`Set.nonempty_Ioc` `isPreconnected_Ioc`
`isConnected_Ioi` 📖	mathematical	—	`IsConnected` `Set.Ioi` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`Set.nonempty_Ioi` `isPreconnected_Ioi`
`isConnected_Ioo` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`IsConnected` `Set.Ioo` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`Set.nonempty_Ioo` `isPreconnected_Ioo`
`isConnected_uIoc` 📖	mathematical	—	`IsConnected` `Set.uIoc` `ConditionallyCompleteLinearOrder.toLinearOrder`	—	`Set.nonempty_uIoc` `isPreconnected_uIoc`
`isConnected_uIoo` 📖	mathematical	—	`IsConnected` `Set.uIoo` `ConditionallyCompleteLinearOrder.toLinearOrder`	—	`Set.nonempty_uIoo` `isPreconnected_uIoo`
`isPreconnected_Icc` 📖	mathematical	—	`IsPreconnected` `Set.Icc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`isPreconnected_closed_iff` `le_total` `isPreconnected_Icc_aux` `Set.inter_comm` `Set.union_comm`
`isPreconnected_Icc_aux` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Set` `Set.instHasSubset` `Set.Icc` `Set.instUnion` `Set.instMembership` `Set.instInter`	`Set.Nonempty` `Set` `Set.instInter` `Set.Icc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`Set.Icc_subset_Icc` `IsClosed.Icc_subset_of_forall_mem_nhdsWithin` `IsClosed.inter` `isClosed_Icc` `OrderTopology.to_orderClosedTopology` `Set.Ico_subset_Icc_self` `nhdsWithin_Ioc_eq_nhdsGT` `instClosedIciTopology` `mem_nhdsWithin` `IsClosed.isOpen_compl` `Set.Subset.rfl` `Filter.mem_of_superset` `le_trans` `le_of_lt` `Set.right_mem_Icc`
`isPreconnected_Ici` 📖	mathematical	—	`IsPreconnected` `Set.Ici` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`Set.OrdConnected.isPreconnected` `Set.ordConnected_Ici`
`isPreconnected_Ico` 📖	mathematical	—	`IsPreconnected` `Set.Ico` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`Set.OrdConnected.isPreconnected` `Set.ordConnected_Ico`
`isPreconnected_Iic` 📖	mathematical	—	`IsPreconnected` `Set.Iic` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`Set.OrdConnected.isPreconnected` `Set.ordConnected_Iic`
`isPreconnected_Iio` 📖	mathematical	—	`IsPreconnected` `Set.Iio` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`Set.OrdConnected.isPreconnected` `Set.ordConnected_Iio`
`isPreconnected_Ioc` 📖	mathematical	—	`IsPreconnected` `Set.Ioc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`Set.OrdConnected.isPreconnected` `Set.ordConnected_Ioc`
`isPreconnected_Ioi` 📖	mathematical	—	`IsPreconnected` `Set.Ioi` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`Set.OrdConnected.isPreconnected` `Set.ordConnected_Ioi`
`isPreconnected_Ioo` 📖	mathematical	—	`IsPreconnected` `Set.Ioo` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`Set.OrdConnected.isPreconnected` `Set.ordConnected_Ioo`
`isPreconnected_iff_ordConnected` 📖	mathematical	—	`IsPreconnected` `Set.OrdConnected` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`IsPreconnected.ordConnected` `OrderTopology.to_orderClosedTopology` `Set.OrdConnected.isPreconnected`
`isPreconnected_uIcc` 📖	mathematical	—	`IsPreconnected` `Set.uIcc` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`isPreconnected_Icc`
`isPreconnected_uIoc` 📖	mathematical	—	`IsPreconnected` `Set.uIoc` `ConditionallyCompleteLinearOrder.toLinearOrder`	—	`isPreconnected_Ioc`
`isPreconnected_uIoo` 📖	mathematical	—	`IsPreconnected` `Set.uIoo` `ConditionallyCompleteLinearOrder.toLinearOrder`	—	`isPreconnected_Ioo`
`isTotallyDisconnected_iff_lt` 📖	mathematical	—	`IsTotallyDisconnected` `Set` `Set.instMembership` `Set.Ioo` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`Set.not_nontrivial_iff` `Set.not_ordConnected_inter_Icc_iff` `Set.inter_subset_left` `le_rfl` `LT.lt.le` `Set.OrdConnected.out'`
`mem_range_of_exists_le_of_exists_ge` 📖	mathematical	`Continuous` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Set` `Set.instMembership` `Set.range`	—	`intermediate_value_univ`
`ordered_connected_space` 📖	mathematical	—	`PreconnectedSpace`	—	`Set.OrdConnected.isPreconnected` `Set.ordConnected_univ`
`setOf_isPreconnected_eq_of_ordered` 📖	mathematical	—	`setOf` `Set` `IsPreconnected` `Set.instUnion` `Set.range` `Set.Icc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Set.Ico` `Set.Ioc` `Set.Ioo` `Set.Ici` `Set.Ioi` `Set.Iic` `Set.Iio` `Set.instInsert` `Set.univ` `Set.instSingletonSet` `Set.instEmptyCollection`	—	`Set.Subset.antisymm` `setOf_isPreconnected_subset_of_ordered` `ordered_connected_space`
`setOf_isPreconnected_subset_of_ordered` 📖	mathematical	—	`Set` `Set.instHasSubset` `setOf` `IsPreconnected` `Set.instUnion` `Set.range` `Set.Icc` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Set.Ico` `Set.Ioc` `Set.Ioo` `Set.Ici` `Set.Ioi` `Set.Iic` `Set.Iio` `Set.instInsert` `Set.univ` `Set.instSingletonSet` `Set.instEmptyCollection`	—	`IsPreconnected.mem_intervals` `Set.union_insert` `Set.union_singleton`

---

← Back to Index