Bounded

📁 Source: Mathlib/Order/Bounded.lean

Statistics

Metric	Count
Definitions	0
Theorems `mono`, `rel_mono`, `mono`, `rel_mono`, `bounded_ge_Icc`, `bounded_ge_Ici`, `bounded_ge_Ico`, `bounded_ge_Ioc`, `bounded_ge_Ioi`, `bounded_ge_Ioo`, `bounded_ge_iff_bounded_gt`, `bounded_ge_inter_ge`, `bounded_ge_inter_gt`, `bounded_ge_inter_not_ge`, `bounded_ge_of_bounded_gt`, `bounded_gt_Icc`, `bounded_gt_Ici`, `bounded_gt_Ico`, `bounded_gt_Ioc`, `bounded_gt_Ioi`, `bounded_gt_Ioo`, `bounded_gt_inter_ge`, `bounded_gt_inter_gt`, `bounded_gt_inter_not_gt`, `bounded_inter_not`, `bounded_le_Icc`, `bounded_le_Ico`, `bounded_le_Iic`, `bounded_le_Iio`, `bounded_le_Ioc`, `bounded_le_Ioo`, `bounded_le_iff_bounded_lt`, `bounded_le_inter_le`, `bounded_le_inter_lt`, `bounded_le_inter_not_le`, `bounded_le_of_bounded_lt`, `bounded_lt_Icc`, `bounded_lt_Ico`, `bounded_lt_Iic`, `bounded_lt_Iio`, `bounded_lt_Ioc`, `bounded_lt_Ioo`, `bounded_lt_inter_le`, `bounded_lt_inter_lt`, `bounded_lt_inter_not_lt`, `bounded_self`, `unbounded_ge_iff`, `unbounded_ge_iff_unbounded_inter_ge`, `unbounded_ge_inter_gt`, `unbounded_ge_inter_not_ge`, `unbounded_ge_of_forall_exists_gt`, `unbounded_ge_univ`, `unbounded_gt_iff`, `unbounded_gt_iff_unbounded_ge`, `unbounded_gt_inter_gt`, `unbounded_gt_inter_not_gt`, `unbounded_gt_of_forall_exists_ge`, `unbounded_gt_of_unbounded_ge`, `unbounded_gt_univ`, `unbounded_inter_ge`, `unbounded_inter_not`, `unbounded_le_Ici`, `unbounded_le_Ioi`, `unbounded_le_iff`, `unbounded_le_inter_le`, `unbounded_le_inter_lt`, `unbounded_le_inter_not_le`, `unbounded_le_of_forall_exists_lt`, `unbounded_le_univ`, `unbounded_lt_Ici`, `unbounded_lt_Ioi`, `unbounded_lt_iff`, `unbounded_lt_iff_unbounded_le`, `unbounded_lt_inter_le`, `unbounded_lt_inter_lt`, `unbounded_lt_inter_not_lt`, `unbounded_lt_of_forall_exists_le`, `unbounded_lt_of_unbounded_le`, `unbounded_lt_univ`	79
Total	79

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bounded_ge_Icc` 📖	mathematical	—	`Bounded` `Preorder.toLE` `Icc`	—	`Bounded.mono` `Icc_subset_Ici_self` `bounded_ge_Ici`
`bounded_ge_Ici` 📖	mathematical	—	`Bounded` `Preorder.toLE` `Ici`	—	`bounded_self`
`bounded_ge_Ico` 📖	mathematical	—	`Bounded` `Preorder.toLE` `Ico`	—	`Bounded.mono` `Ico_subset_Ici_self` `bounded_ge_Ici`
`bounded_ge_Ioc` 📖	mathematical	—	`Bounded` `Preorder.toLE` `Ioc`	—	`Bounded.mono` `Ioc_subset_Ioi_self` `bounded_ge_Ioi`
`bounded_ge_Ioi` 📖	mathematical	—	`Bounded` `Preorder.toLE` `Ioi`	—	`bounded_ge_of_bounded_gt` `bounded_gt_Ioi`
`bounded_ge_Ioo` 📖	mathematical	—	`Bounded` `Preorder.toLE` `Ioo`	—	`Bounded.mono` `Ioo_subset_Ioi_self` `bounded_ge_Ioi`
`bounded_ge_iff_bounded_gt` 📖	mathematical	—	`Bounded` `Preorder.toLE` `Preorder.toLT`	—	`bounded_le_iff_bounded_lt` `OrderDual.noMaxOrder`
`bounded_ge_inter_ge` 📖	mathematical	—	`Bounded` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `instInter` `setOf`	—	`bounded_le_inter_le`
`bounded_ge_inter_gt` 📖	mathematical	—	`Bounded` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `instInter` `setOf` `Preorder.toLT`	—	`bounded_le_inter_lt`
`bounded_ge_inter_not_ge` 📖	mathematical	—	`Bounded` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Set` `instInter` `setOf`	—	`bounded_le_inter_not_le`
`bounded_ge_of_bounded_gt` 📖	mathematical	`Bounded` `Preorder.toLT`	`Preorder.toLE`	—	`le_of_lt`
`bounded_gt_Icc` 📖	mathematical	—	`Bounded` `Preorder.toLT` `Icc`	—	`Bounded.mono` `Icc_subset_Ici_self` `bounded_gt_Ici`
`bounded_gt_Ici` 📖	mathematical	—	`Bounded` `Preorder.toLT` `Ici`	—	—
`bounded_gt_Ico` 📖	mathematical	—	`Bounded` `Preorder.toLT` `Ico`	—	`Bounded.mono` `Ico_subset_Ici_self` `bounded_gt_Ici`
`bounded_gt_Ioc` 📖	mathematical	—	`Bounded` `Preorder.toLT` `Ioc`	—	`Bounded.mono` `Ioc_subset_Ioi_self` `bounded_gt_Ioi`
`bounded_gt_Ioi` 📖	mathematical	—	`Bounded` `Preorder.toLT` `Ioi`	—	`bounded_self`
`bounded_gt_Ioo` 📖	mathematical	—	`Bounded` `Preorder.toLT` `Ioo`	—	`Bounded.mono` `Ioo_subset_Ioi_self` `bounded_gt_Ioi`
`bounded_gt_inter_ge` 📖	mathematical	—	`Bounded` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `instInter` `setOf` `Preorder.toLE`	—	`bounded_lt_inter_le`
`bounded_gt_inter_gt` 📖	mathematical	—	`Bounded` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `instInter` `setOf`	—	`bounded_lt_inter_lt` `OrderDual.noMaxOrder`
`bounded_gt_inter_not_gt` 📖	mathematical	—	`Bounded` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Set` `instInter` `setOf`	—	`bounded_lt_inter_not_lt`
`bounded_inter_not` 📖	mathematical	—	`Bounded` `Set` `instInter` `setOf`	—	`Bounded.mono` `inter_subset_left`
`bounded_le_Icc` 📖	mathematical	—	`Bounded` `Preorder.toLE` `Icc`	—	`Bounded.mono` `Icc_subset_Iic_self` `bounded_le_Iic`
`bounded_le_Ico` 📖	mathematical	—	`Bounded` `Preorder.toLE` `Ico`	—	`Bounded.mono` `Ico_subset_Iio_self` `bounded_le_Iio`
`bounded_le_Iic` 📖	mathematical	—	`Bounded` `Preorder.toLE` `Iic`	—	`bounded_self`
`bounded_le_Iio` 📖	mathematical	—	`Bounded` `Preorder.toLE` `Iio`	—	`bounded_le_of_bounded_lt` `bounded_lt_Iio`
`bounded_le_Ioc` 📖	mathematical	—	`Bounded` `Preorder.toLE` `Ioc`	—	`Bounded.mono` `Ioc_subset_Iic_self` `bounded_le_Iic`
`bounded_le_Ioo` 📖	mathematical	—	`Bounded` `Preorder.toLE` `Ioo`	—	`Bounded.mono` `Ioo_subset_Iio_self` `bounded_le_Iio`
`bounded_le_iff_bounded_lt` 📖	mathematical	—	`Bounded` `Preorder.toLE` `Preorder.toLT`	—	`NoMaxOrder.exists_gt` `lt_of_le_of_lt` `bounded_le_of_bounded_lt`
`bounded_le_inter_le` 📖	mathematical	—	`Bounded` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `instInter` `setOf`	—	`bounded_le_inter_lt` `Bounded.mono` `le_of_lt` `inter_subset_left`
`bounded_le_inter_lt` 📖	mathematical	—	`Bounded` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `instInter` `setOf` `Preorder.toLT`	—	—
`bounded_le_inter_not_le` 📖	mathematical	—	`Bounded` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Set` `instInter` `setOf`	—	`bounded_inter_not` `le_sup_of_le_left` `le_sup_of_le_right`
`bounded_le_of_bounded_lt` 📖	mathematical	`Bounded` `Preorder.toLT`	`Preorder.toLE`	—	`Bounded.rel_mono` `le_of_lt`
`bounded_lt_Icc` 📖	mathematical	—	`Bounded` `Preorder.toLT` `Icc`	—	`Bounded.mono` `Icc_subset_Iic_self` `bounded_lt_Iic`
`bounded_lt_Ico` 📖	mathematical	—	`Bounded` `Preorder.toLT` `Ico`	—	`Bounded.mono` `Ico_subset_Iio_self` `bounded_lt_Iio`
`bounded_lt_Iic` 📖	mathematical	—	`Bounded` `Preorder.toLT` `Iic`	—	—
`bounded_lt_Iio` 📖	mathematical	—	`Bounded` `Preorder.toLT` `Iio`	—	`bounded_self`
`bounded_lt_Ioc` 📖	mathematical	—	`Bounded` `Preorder.toLT` `Ioc`	—	`Bounded.mono` `Ioc_subset_Iic_self` `bounded_lt_Iic`
`bounded_lt_Ioo` 📖	mathematical	—	`Bounded` `Preorder.toLT` `Ioo`	—	`Bounded.mono` `Ioo_subset_Iio_self` `bounded_lt_Iio`
`bounded_lt_inter_le` 📖	mathematical	—	`Bounded` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `instInter` `setOf` `Preorder.toLE`	—	`not_lt` `bounded_lt_inter_not_lt`
`bounded_lt_inter_lt` 📖	mathematical	—	`Bounded` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `instInter` `setOf`	—	`bounded_le_iff_bounded_lt` `bounded_le_inter_lt`
`bounded_lt_inter_not_lt` 📖	mathematical	—	`Bounded` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Set` `instInter` `setOf`	—	`bounded_inter_not` `lt_sup_of_lt_left` `lt_sup_of_lt_right`
`bounded_self` 📖	mathematical	—	`Bounded` `setOf`	—	—
`unbounded_ge_iff` 📖	mathematical	—	`Unbounded` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `instMembership` `Preorder.toLT`	—	`lt_of_not_ge` `unbounded_ge_of_forall_exists_gt`
`unbounded_ge_iff_unbounded_inter_ge` 📖	mathematical	—	`Unbounded` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `instInter` `setOf`	—	`unbounded_le_inter_le`
`unbounded_ge_inter_gt` 📖	mathematical	—	`Unbounded` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `instInter` `setOf` `Preorder.toLT`	—	`unbounded_le_inter_lt`
`unbounded_ge_inter_not_ge` 📖	mathematical	—	`Unbounded` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Set` `instInter` `setOf`	—	`unbounded_le_inter_not_le`
`unbounded_ge_of_forall_exists_gt` 📖	mathematical	`Set` `instMembership` `Preorder.toLT`	`Unbounded` `Preorder.toLE`	—	`unbounded_le_of_forall_exists_lt`
`unbounded_ge_univ` 📖	mathematical	—	`Unbounded` `univ`	—	`NoBotOrder.exists_not_ge`
`unbounded_gt_iff` 📖	mathematical	—	`Unbounded` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `instMembership` `Preorder.toLE`	—	`le_of_not_gt` `unbounded_gt_of_forall_exists_ge`
`unbounded_gt_iff_unbounded_ge` 📖	mathematical	—	`Unbounded` `Preorder.toLT` `Preorder.toLE`	—	`unbounded_lt_iff_unbounded_le` `OrderDual.noMaxOrder`
`unbounded_gt_inter_gt` 📖	mathematical	—	`Unbounded` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `instInter` `setOf`	—	`unbounded_lt_inter_lt` `OrderDual.noMaxOrder`
`unbounded_gt_inter_not_gt` 📖	mathematical	—	`Unbounded` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Set` `instInter` `setOf`	—	`unbounded_lt_inter_not_lt`
`unbounded_gt_of_forall_exists_ge` 📖	mathematical	`Set` `instMembership` `Preorder.toLE`	`Unbounded` `Preorder.toLT`	—	`not_le_of_gt`
`unbounded_gt_of_unbounded_ge` 📖	mathematical	`Unbounded` `Preorder.toLE`	`Preorder.toLT`	—	`le_of_lt`
`unbounded_gt_univ` 📖	mathematical	—	`Unbounded` `Preorder.toLT` `univ`	—	`unbounded_gt_of_unbounded_ge` `unbounded_ge_univ`
`unbounded_inter_ge` 📖	mathematical	—	`Unbounded` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `instInter` `setOf` `Preorder.toLE`	—	`unbounded_lt_inter_le`
`unbounded_inter_not` 📖	mathematical	—	`Unbounded` `Set` `instInter` `setOf`	—	`bounded_inter_not`
`unbounded_le_Ici` 📖	mathematical	—	`Unbounded` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Ici`	—	`Unbounded.mono` `Ioi_subset_Ici_self` `unbounded_le_Ioi`
`unbounded_le_Ioi` 📖	mathematical	—	`Unbounded` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Ioi`	—	`NoMaxOrder.exists_gt` `LE.le.trans_lt` `le_sup_left` `LT.lt.not_ge` `le_sup_right`
`unbounded_le_iff` 📖	mathematical	—	`Unbounded` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `instMembership` `Preorder.toLT`	—	—
`unbounded_le_inter_le` 📖	mathematical	—	`Unbounded` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `instInter` `setOf`	—	`not_bounded_iff` `not_iff_not` `bounded_le_inter_le`
`unbounded_le_inter_lt` 📖	mathematical	—	`Unbounded` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `instInter` `setOf` `Preorder.toLT`	—	`lt_iff_not_ge` `unbounded_le_inter_not_le`
`unbounded_le_inter_not_le` 📖	mathematical	—	`Unbounded` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Set` `instInter` `setOf`	—	`not_bounded_iff` `not_iff_not` `bounded_le_inter_not_le`
`unbounded_le_of_forall_exists_lt` 📖	mathematical	`Set` `instMembership` `Preorder.toLT`	`Unbounded` `Preorder.toLE`	—	`LE.le.not_gt`
`unbounded_le_univ` 📖	mathematical	—	`Unbounded` `univ`	—	`NoTopOrder.exists_not_le`
`unbounded_lt_Ici` 📖	mathematical	—	`Unbounded` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Ici`	—	`le_sup_left` `LE.le.not_gt` `le_sup_right`
`unbounded_lt_Ioi` 📖	mathematical	—	`Unbounded` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Ioi`	—	`unbounded_lt_of_unbounded_le` `unbounded_le_Ioi`
`unbounded_lt_iff` 📖	mathematical	—	`Unbounded` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `instMembership` `Preorder.toLE`	—	—
`unbounded_lt_iff_unbounded_le` 📖	mathematical	—	`Unbounded` `Preorder.toLT` `Preorder.toLE`	—	—
`unbounded_lt_inter_le` 📖	mathematical	—	`Unbounded` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `instInter` `setOf` `Preorder.toLE`	—	`not_lt` `unbounded_lt_inter_not_lt`
`unbounded_lt_inter_lt` 📖	mathematical	—	`Unbounded` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `instInter` `setOf`	—	`not_bounded_iff` `not_iff_not` `bounded_lt_inter_lt`
`unbounded_lt_inter_not_lt` 📖	mathematical	—	`Unbounded` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Set` `instInter` `setOf`	—	`not_bounded_iff` `not_iff_not` `bounded_lt_inter_not_lt`
`unbounded_lt_of_forall_exists_le` 📖	mathematical	`Set` `instMembership` `Preorder.toLE`	`Unbounded` `Preorder.toLT`	—	`LT.lt.not_ge`
`unbounded_lt_of_unbounded_le` 📖	mathematical	`Unbounded` `Preorder.toLE`	`Preorder.toLT`	—	`Unbounded.rel_mono` `le_of_lt`
`unbounded_lt_univ` 📖	mathematical	—	`Unbounded` `Preorder.toLT` `univ`	—	`unbounded_lt_of_unbounded_le` `unbounded_le_univ`

Set.Bounded

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mono` 📖	—	`Set` `Set.instHasSubset` `Set.Bounded`	—	—	—
`rel_mono` 📖	—	`Set.Bounded` `Pi.hasLe` `Prop.le`	—	—	—

Set.Unbounded

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mono` 📖	—	`Set` `Set.instHasSubset` `Set.Unbounded`	—	—	—
`rel_mono` 📖	—	`Pi.hasLe` `Prop.le` `Set.Unbounded`	—	—	—

---

← Back to Index