OrdConnected

📁 Source: Mathlib/Order/Interval/Set/OrdConnected.lean

Statistics

Metric	Count
Definitions `OrdConnected`	1
Theorems `ordConnected`, `image_Icc`, `image_Ico`, `image_Ioc`, `image_Ioo`, `Icc_subset`, `dual`, `inter`, `inter'`, `out`, `preimage_anti`, `preimage_antitoneOn`, `preimage_mono`, `preimage_monotoneOn`, `uIcc_subset`, `uIoc_subset`, `dual_ordConnected`, `dual_ordConnected_iff`, `image_subtype_val_Icc`, `image_subtype_val_Ico`, `image_subtype_val_Ioc`, `image_subtype_val_Ioo`, `image_subtype_val_uIcc`, `image_subtype_val_uIoc`, `image_subtype_val_uIoo`, `instDenselyOrdered`, `not_ordConnected_inter_Icc_iff`, `ordConnected_Icc`, `ordConnected_Ici`, `ordConnected_Ico`, `ordConnected_Iic`, `ordConnected_Iio`, `ordConnected_Ioc`, `ordConnected_Ioi`, `ordConnected_Ioo`, `ordConnected_biInter`, `ordConnected_def`, `ordConnected_dual`, `ordConnected_empty`, `ordConnected_iInter`, `ordConnected_iInter'`, `ordConnected_iff`, `ordConnected_iff_uIcc_subset`, `ordConnected_iff_uIcc_subset_left`, `ordConnected_iff_uIcc_subset_right`, `ordConnected_image`, `ordConnected_inter_Icc_iff`, `ordConnected_inter_Icc_of_subset`, `ordConnected_of_Ioo`, `ordConnected_of_uIcc_subset_left`, `ordConnected_pi`, `ordConnected_pi'`, `ordConnected_preimage`, `ordConnected_range`, `ordConnected_sInter`, `ordConnected_singleton`, `ordConnected_uIcc`, `ordConnected_uIoc`, `ordConnected_univ`	59
Total	60

IsAntichain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ordConnected` 📖	mathematical	`IsAntichain` `Preorder.toLE` `PartialOrder.toPreorder`	`Set.OrdConnected`	—	`Set.mem_singleton_iff` `Set.Icc_self` `eq` `LE.le.trans`

OrderEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`image_Icc` 📖	mathematical	—	`Set.image` `DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `instFunLikeOrderEmbedding` `Set.Icc`	—	`preimage_Icc` `Set.image_preimage_eq_inter_range` `Set.inter_eq_left` `Set.OrdConnected.out`
`image_Ico` 📖	mathematical	—	`Set.image` `DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `instFunLikeOrderEmbedding` `Set.Ico`	—	`preimage_Ico` `Set.image_preimage_eq_inter_range` `Set.inter_eq_left` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.Ico_subset_Icc_self` `Set.OrdConnected.out`
`image_Ioc` 📖	mathematical	—	`Set.image` `DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `instFunLikeOrderEmbedding` `Set.Ioc`	—	`preimage_Ioc` `Set.image_preimage_eq_inter_range` `Set.inter_eq_left` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.Ioc_subset_Icc_self` `Set.OrdConnected.out`
`image_Ioo` 📖	mathematical	—	`Set.image` `DFunLike.coe` `OrderEmbedding` `Preorder.toLE` `instFunLikeOrderEmbedding` `Set.Ioo`	—	`preimage_Ioo` `Set.image_preimage_eq_inter_range` `Set.inter_eq_left` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.Ioo_subset_Icc_self` `Set.OrdConnected.out`

Set

Definitions

Name	Category	Theorems
`OrdConnected` 📖	CompData	76 math math: `convex_iff_ordConnected`, `OrdConnected.preimage_antitoneOn`, `ordConnected_preimage`, `isPreconnected_iff_ordConnected`, `Finset.ordConnected_range_coe`, `OrdConnected.IicExtend`, `ordConnected_range`, `ordConnected_Ioi`, `ordConnected_iff_uIcc_subset_left`, `OrdConnected.image_deriv`, `starConvex_iff_ordConnected`, `Finset.ordConnected_range_val`, `ordConnected_Iic`, `IsLowerSet.ordConnected`, `IsAntichain.ordConnected`, `ordConnected_Ici`, `ordConnected_def`, `OrdConnected.vadd`, `ordConnected_Ico`, `OrdConnected.smul`, `Nonempty.ordConnected_iff_of_bdd'`, `OrdConnected.image_ennreal_ofReal`, `OrdConnected.preimage_anti`, `ordConnected_iff_disjoint_Ioo_empty`, `OrdConnected.image_derivWithin`, `ordConnected_Ioc`, `dual_ordConnected`, `EMetric.ordConnected_setOf_closedBall_subset`, `ordConnected_univ`, `IsPreconnected.ordConnected`, `ordConnected_image`, `Metric.ordConnected_setOf_closedEBall_subset`, `ordConnected_Icc`, `OrdConnected.interior`, `OrdConnected.image_coe_nnreal_real`, `OrdConnected.preimage_coe_nnreal_ennreal`, `Nonempty.ordConnected_iff_of_bdd`, `OrdConnected.IciExtend`, `OrdConnected.restrict`, `ordConnected_iff_upperClosure_inter_lowerClosure`, `not_ordConnected_inter_Icc_iff`, `ordConnected_of_uIcc_subset_left`, `OrdConnected.image_real_toNNReal`, `ordConnected_dual`, `strictConvex_iff_ordConnected`, `IsUpperSet.ordConnected`, `ordConnected_inter_Icc_of_subset`, `Metric.ordConnected_setOf_eball_subset`, `OrdConnected.preimage_ennreal_ofReal`, `ordConnected_singleton`, `OrdConnected.dual`, `OrdConnected.inter`, `ordConnected_iff_uIcc_subset_right`, `Convex.ordConnected`, `OrdConnected.preimage_real_toNNReal`, `OrdConnected.preimage_mono`, `OrdConnected.preimage_coe_nnreal_real`, `ordConnected_inter_Icc_iff`, `ArchimedeanClass.FiniteResidueField.ordConnected_preimage_mk`, `ordConnected_Ioo`, `EMetric.ordConnected_setOf_ball_subset`, `ordConnected_Iio`, `dual_ordConnected_iff`, `ordConnected_iff_uIcc_subset`, `ordConnected_iff`, `StarConvex.ordConnected`, `OrdConnected.image_hasDerivWithinAt`, `OrdConnected.inter'`, `ordConnected_empty`, `OrdConnected.image_coe_nnreal_ennreal`, `ordConnected_of_Ioo`, `instOrdConnectedOrdConnectedComponent`, `StrictConvex.ordConnected`, `ordConnected_uIoc`, `OrdConnected.preimage_monotoneOn`, `ordConnected_uIcc`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Icc_subset` 📖	mathematical	`Set` `instMembership`	`instHasSubset` `Icc`	—	`OrdConnected.out`
`dual_ordConnected` 📖	mathematical	—	`OrdConnected` `OrderDual` `OrderDual.instPreorder` `preimage` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual`	—	`OrdConnected.dual`
`dual_ordConnected_iff` 📖	mathematical	—	`OrdConnected` `OrderDual` `OrderDual.instPreorder` `preimage` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual`	—	`ordConnected_dual`
`image_subtype_val_Icc` 📖	mathematical	—	`image` `Set` `instMembership` `Icc` `Subtype.preorder`	—	`OrderEmbedding.image_Icc` `Subtype.range_coe_subtype`
`image_subtype_val_Ico` 📖	mathematical	—	`image` `Set` `instMembership` `Ico` `Subtype.preorder`	—	`OrderEmbedding.image_Ico` `Subtype.range_coe_subtype`
`image_subtype_val_Ioc` 📖	mathematical	—	`image` `Set` `instMembership` `Ioc` `Subtype.preorder`	—	`OrderEmbedding.image_Ioc` `Subtype.range_coe_subtype`
`image_subtype_val_Ioo` 📖	mathematical	—	`image` `Set` `instMembership` `Ioo` `Subtype.preorder`	—	`OrderEmbedding.image_Ioo` `Subtype.range_coe_subtype`
`image_subtype_val_uIcc` 📖	mathematical	—	`image` `Set` `instMembership` `uIcc` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Subtype.instLinearOrder`	—	`image_subtype_val_Icc` `Monotone.map_inf` `Subtype.mono_coe` `Monotone.map_sup`
`image_subtype_val_uIoc` 📖	mathematical	—	`image` `Set` `instMembership` `uIoc` `Subtype.instLinearOrder`	—	`image_subtype_val_Ioc` `Monotone.map_inf` `Subtype.mono_coe` `Monotone.map_sup`
`image_subtype_val_uIoo` 📖	mathematical	—	`image` `Set` `instMembership` `uIoo` `Subtype.instLinearOrder`	—	`image_subtype_val_Ioo` `Monotone.map_inf` `Subtype.mono_coe` `Monotone.map_sup`
`instDenselyOrdered` 📖	mathematical	—	`DenselyOrdered` `Elem` `Preorder.toLT` `Set` `instMembership`	—	`exists_between` `OrdConnected.out` `Ioo_subset_Icc_self`
`not_ordConnected_inter_Icc_iff` 📖	mathematical	`Set` `instMembership`	`OrdConnected` `PartialOrder.toPreorder` `instInter` `Icc` `Ioo`	—	`ordConnected_inter_Icc_iff`
`ordConnected_Icc` 📖	mathematical	—	`OrdConnected` `Icc`	—	`OrdConnected.inter` `ordConnected_Ici` `ordConnected_Iic`
`ordConnected_Ici` 📖	mathematical	—	`OrdConnected` `Ici`	—	`le_trans`
`ordConnected_Ico` 📖	mathematical	—	`OrdConnected` `Ico`	—	`OrdConnected.inter` `ordConnected_Ici` `ordConnected_Iio`
`ordConnected_Iic` 📖	mathematical	—	`OrdConnected` `Iic`	—	`le_trans`
`ordConnected_Iio` 📖	mathematical	—	`OrdConnected` `Iio`	—	`lt_of_le_of_lt`
`ordConnected_Ioc` 📖	mathematical	—	`OrdConnected` `Ioc`	—	`OrdConnected.inter` `ordConnected_Ioi` `ordConnected_Iic`
`ordConnected_Ioi` 📖	mathematical	—	`OrdConnected` `Ioi`	—	`lt_of_lt_of_le`
`ordConnected_Ioo` 📖	mathematical	—	`OrdConnected` `Ioo`	—	`OrdConnected.inter` `ordConnected_Ioi` `ordConnected_Iio`
`ordConnected_biInter` 📖	mathematical	`OrdConnected`	`iInter`	—	`ordConnected_iInter`
`ordConnected_def` 📖	mathematical	—	`OrdConnected` `Set` `instHasSubset` `Icc`	—	`OrdConnected.out'`
`ordConnected_dual` 📖	mathematical	—	`OrdConnected` `OrderDual` `OrderDual.instPreorder` `preimage` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual`	—	`OrdConnected.dual`
`ordConnected_empty` 📖	mathematical	—	`OrdConnected` `Set` `instEmptyCollection`	—	—
`ordConnected_iInter` 📖	mathematical	`OrdConnected`	`iInter`	—	`ordConnected_sInter` `forall_mem_range`
`ordConnected_iInter'` 📖	mathematical	`OrdConnected`	`iInter`	—	`ordConnected_iInter`
`ordConnected_iff` 📖	mathematical	—	`OrdConnected` `Set` `instHasSubset` `Icc`	—	`ordConnected_def` `le_trans`
`ordConnected_iff_uIcc_subset` 📖	mathematical	—	`OrdConnected` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `instHasSubset` `uIcc`	—	`OrdConnected.uIcc_subset` `HasSubset.Subset.trans` `instIsTransSubset` `Icc_subset_uIcc`
`ordConnected_iff_uIcc_subset_left` 📖	mathematical	`Set` `instMembership`	`OrdConnected` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instHasSubset` `uIcc`	—	`OrdConnected.uIcc_subset` `ordConnected_of_uIcc_subset_left`
`ordConnected_iff_uIcc_subset_right` 📖	mathematical	`Set` `instMembership`	`OrdConnected` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instHasSubset` `uIcc`	—	`ordConnected_iff_uIcc_subset_left` `uIcc_comm`
`ordConnected_image` 📖	mathematical	—	`OrdConnected` `image` `DFunLike.coe` `EquivLike.toFunLike`	—	`OrderIso.image_eq_preimage_symm` `ordConnected_preimage` `RelIso.instRelHomClass`
`ordConnected_inter_Icc_iff` 📖	mathematical	`Set` `instMembership`	`OrdConnected` `PartialOrder.toPreorder` `instInter` `Icc` `instHasSubset` `Ioo`	—	`HasSubset.Subset.trans` `instIsTransSubset` `Ioo_subset_Icc_self` `LE.le.trans` `OrdConnected.out` `left_mem_Icc` `right_mem_Icc` `ordConnected_inter_Icc_of_subset`
`ordConnected_inter_Icc_of_subset` 📖	mathematical	`Set` `instHasSubset` `Ioo` `PartialOrder.toPreorder`	`OrdConnected` `instInter` `Icc`	—	`ordConnected_of_Ioo` `HasSubset.Subset.trans` `instIsTransSubset` `Ioo_subset_Ioo` `subset_inter` `Ioo_subset_Icc_self`
`ordConnected_of_Ioo` 📖	mathematical	`Set` `instHasSubset` `Ioo` `PartialOrder.toPreorder`	`OrdConnected`	—	`ordConnected_iff` `eq_or_lt_of_le` `Icc_self` `Ioc_insert_left` `Ioo_insert_right` `insert_subset_iff`
`ordConnected_of_uIcc_subset_left` 📖	mathematical	`Set` `instHasSubset` `uIcc` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`OrdConnected` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf`	—	`ordConnected_iff_uIcc_subset` `uIcc_subset_uIcc_union_uIcc` `uIcc_comm` `union_subset`
`ordConnected_pi` 📖	mathematical	`OrdConnected`	`Pi.preorder` `pi`	—	`OrdConnected.out`
`ordConnected_pi'` 📖	mathematical	`OrdConnected`	`Pi.preorder` `pi`	—	`ordConnected_pi`
`ordConnected_preimage` 📖	mathematical	—	`OrdConnected` `preimage` `DFunLike.coe`	—	`OrdConnected.out` `OrderHomClass.mono`
`ordConnected_range` 📖	mathematical	—	`OrdConnected` `range` `DFunLike.coe` `EquivLike.toFunLike`	—	`ordConnected_image` `OrderIso.instOrderIsoClass` `ordConnected_univ`
`ordConnected_sInter` 📖	mathematical	`OrdConnected`	`sInter`	—	`OrdConnected.out`
`ordConnected_singleton` 📖	mathematical	—	`OrdConnected` `PartialOrder.toPreorder` `Set` `instSingletonSet`	—	`Icc_self` `ordConnected_Icc`
`ordConnected_uIcc` 📖	mathematical	—	`OrdConnected` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `uIcc`	—	`ordConnected_Icc`
`ordConnected_uIoc` 📖	mathematical	—	`OrdConnected` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `uIoc`	—	`ordConnected_Ioc`
`ordConnected_univ` 📖	mathematical	—	`OrdConnected` `univ`	—	`subset_univ`

Set.OrdConnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dual` 📖	mathematical	—	`Set.OrdConnected` `OrderDual` `OrderDual.instPreorder` `Set.preimage` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual`	—	`out`
`inter` 📖	mathematical	—	`Set.OrdConnected` `Set` `Set.instInter`	—	`Set.subset_inter` `out`
`inter'` 📖	mathematical	—	`Set.OrdConnected` `Set` `Set.instInter`	—	`inter`
`out` 📖	mathematical	`Set` `Set.instMembership`	`Set.instHasSubset` `Set.Icc`	—	`out'`
`preimage_anti` 📖	mathematical	`Antitone`	`Set.OrdConnected` `Set.preimage`	—	`out`
`preimage_antitoneOn` 📖	mathematical	`AntitoneOn`	`Set.OrdConnected` `Set` `Set.instInter` `Set.preimage`	—	`preimage_monotoneOn` `dual` `AntitoneOn.dual_right`
`preimage_mono` 📖	mathematical	`Monotone`	`Set.OrdConnected` `Set.preimage`	—	`out`
`preimage_monotoneOn` 📖	mathematical	`MonotoneOn`	`Set.OrdConnected` `Set` `Set.instInter` `Set.preimage`	—	`LE.le.trans` `Set.Subset.antisymm` `le_rfl` `out`
`uIcc_subset` 📖	mathematical	`Set` `Set.instMembership`	`Set.instHasSubset` `Set.uIcc` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`out` `min_rec'` `max_rec'`
`uIoc_subset` 📖	mathematical	`Set` `Set.instMembership`	`Set.instHasSubset` `Set.uIoc`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.Ioc_subset_Icc_self` `uIcc_subset`

---

← Back to Index