Basic

📁 Source: Mathlib/Order/UpperLower/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems `Iic_subset`, `Iio_subset`, `bot_mem`, `bot_notMem`, `compl`, `eq_empty_or_Iic`, `eq_univ_or_Iio`, `erase`, `image`, `inter`, `isUpperSet_preimage_coe`, `lowerBounds_subset`, `not_bddBelow`, `ofDual`, `ordConnected`, `preimage`, `sdiff`, `sdiff_of_isUpperSet`, `toDual`, `top_mem`, `total`, `union`, `Ici_subset`, `Ioi_subset`, `bot_mem`, `compl`, `eq_empty_or_Ici`, `eq_univ_or_Ioi`, `erase`, `image`, `inter`, `isLowerSet_preimage_coe`, `not_bddAbove`, `ofDual`, `ordConnected`, `preimage`, `sdiff`, `sdiff_of_isLowerSet`, `toDual`, `top_mem`, `top_notMem`, `total`, `union`, `upperBounds_subset`, `image_Ici`, `image_Iic`, `image_Iio`, `image_Ioi`, `antitone_mem`, `monotone_mem`, `isLowerSet_Iic`, `isLowerSet_Iio`, `isLowerSet_compl`, `isLowerSet_empty`, `isLowerSet_iInter`, `isLowerSet_iInter₂`, `isLowerSet_iUnion`, `isLowerSet_iUnion₂`, `isLowerSet_iff_Iic_subset`, `isLowerSet_iff_Iio_subset`, `isLowerSet_iff_forall_lt`, `isLowerSet_preimage_ofDual_iff`, `isLowerSet_preimage_toDual_iff`, `isLowerSet_sInter`, `isLowerSet_sUnion`, `isLowerSet_setOf`, `isLowerSet_univ`, `isUpperSet_Ici`, `isUpperSet_Ioi`, `isUpperSet_compl`, `isUpperSet_empty`, `isUpperSet_iInter`, `isUpperSet_iInter₂`, `isUpperSet_iUnion`, `isUpperSet_iUnion₂`, `isUpperSet_iff_Ici_subset`, `isUpperSet_iff_Ioi_subset`, `isUpperSet_iff_forall_lt`, `isUpperSet_preimage_ofDual_iff`, `isUpperSet_preimage_toDual_iff`, `isUpperSet_sInter`, `isUpperSet_sUnion`, `isUpperSet_setOf`, `isUpperSet_univ`, `not_bddAbove_Ici`, `not_bddAbove_Ioi`, `not_bddBelow_Iic`, `not_bddBelow_Iio`	88
Total	88

IsLowerSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Iic_subset` 📖	mathematical	`IsLowerSet` `Preorder.toLE` `Set` `Set.instMembership`	`Set.instHasSubset` `Set.Iic`	—	`isLowerSet_iff_Iic_subset`
`Iio_subset` 📖	mathematical	`IsLowerSet` `Preorder.toLE` `Set` `Set.instMembership`	`Set.instHasSubset` `Set.Iio`	—	`IsUpperSet.Ioi_subset` `toDual`
`bot_mem` 📖	mathematical	`IsLowerSet` `Preorder.toLE`	`Set` `Set.instMembership` `Bot.bot` `OrderBot.toBot` `Set.Nonempty`	—	`bot_le`
`bot_notMem` 📖	mathematical	`IsLowerSet` `Preorder.toLE`	`Set` `Set.instMembership` `Bot.bot` `OrderBot.toBot` `Set.instEmptyCollection`	—	`Iff.not` `bot_mem` `Set.not_nonempty_iff_eq_empty`
`compl` 📖	mathematical	`IsLowerSet`	`IsUpperSet` `Compl.compl` `Set` `Set.instCompl`	—	—
`eq_empty_or_Iic` 📖	mathematical	`IsLowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Set` `Set.instEmptyCollection` `Set.Iic`	—	`IsUpperSet.eq_empty_or_Ici` `IsWellOrder.toIsWellFounded` `isWellOrder_lt` `instWellFoundedLTOrderDualOfWellFoundedGT`
`eq_univ_or_Iio` 📖	mathematical	`IsLowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Set.univ` `Set.Iio`	—	`compl_inj_iff` `Set.compl_univ` `Set.compl_Iio` `IsUpperSet.eq_empty_or_Ici` `compl`
`erase` 📖	mathematical	`IsLowerSet`	`Set` `Set.instSDiff` `Set.instSingletonSet`	—	`sdiff` `Set.mem_singleton_iff`
`image` 📖	mathematical	`IsLowerSet` `Preorder.toLE`	`Set.image` `DFunLike.coe` `OrderIso` `instFunLikeOrderIso`	—	`Equiv.image_eq_preimage_symm` `preimage` `OrderIso.monotone`
`inter` 📖	mathematical	`IsLowerSet`	`Set` `Set.instInter`	—	—
`isUpperSet_preimage_coe` 📖	mathematical	`IsLowerSet`	`IsUpperSet` `Set.Elem` `Set` `Set.instMembership` `Set.preimage`	—	`Set.mem_preimage`
`lowerBounds_subset` 📖	mathematical	`IsLowerSet` `Preorder.toLE` `Set.Nonempty`	`Set` `Set.instHasSubset` `lowerBounds`	—	—
`not_bddBelow` 📖	mathematical	`IsLowerSet` `Preorder.toLE` `Set.Nonempty`	`BddBelow`	—	`NoMinOrder.exists_lt` `LT.lt.not_ge` `LE.le.trans` `LT.lt.le`
`ofDual` 📖	mathematical	`IsLowerSet` `OrderDual` `OrderDual.instLE`	`IsUpperSet` `Set.preimage` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	`isUpperSet_preimage_toDual_iff`
`ordConnected` 📖	mathematical	`IsLowerSet` `Preorder.toLE`	`Set.OrdConnected`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.Icc_subset_Iic_self` `Iic_subset`
`preimage` 📖	mathematical	`IsLowerSet` `Preorder.toLE` `Monotone`	`Set.preimage`	—	—
`sdiff` 📖	mathematical	`IsLowerSet` `Set` `Set.instMembership`	`Set.instSDiff`	—	—
`sdiff_of_isUpperSet` 📖	mathematical	`IsLowerSet` `IsUpperSet`	`Set` `Set.instSDiff`	—	`sdiff`
`toDual` 📖	mathematical	`IsLowerSet`	`IsUpperSet` `OrderDual` `OrderDual.instLE` `Set.preimage` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual`	—	`isUpperSet_preimage_ofDual_iff`
`top_mem` 📖	mathematical	`IsLowerSet` `Preorder.toLE`	`Set` `Set.instMembership` `Top.top` `OrderTop.toTop` `Set.univ`	—	`Set.eq_univ_of_forall` `le_top` `Set.mem_univ`
`total` 📖	mathematical	`IsLowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Set` `Set.instHasSubset`	—	`Set.not_subset` `le_total`
`union` 📖	mathematical	`IsLowerSet`	`Set` `Set.instUnion`	—	—

IsUpperSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Ici_subset` 📖	mathematical	`IsUpperSet` `Preorder.toLE` `Set` `Set.instMembership`	`Set.instHasSubset` `Set.Ici`	—	`isUpperSet_iff_Ici_subset`
`Ioi_subset` 📖	mathematical	`IsUpperSet` `Preorder.toLE` `Set` `Set.instMembership`	`Set.instHasSubset` `Set.Ioi`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.Ioi_subset_Ici_self` `Ici_subset`
`bot_mem` 📖	mathematical	`IsUpperSet` `Preorder.toLE`	`Set` `Set.instMembership` `Bot.bot` `OrderBot.toBot` `Set.univ`	—	`Set.eq_univ_of_forall` `bot_le` `Set.mem_univ`
`compl` 📖	mathematical	`IsUpperSet`	`IsLowerSet` `Compl.compl` `Set` `Set.instCompl`	—	—
`eq_empty_or_Ici` 📖	mathematical	`IsUpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Set` `Set.instEmptyCollection` `Set.Ici`	—	`Set.nonempty_iff_ne_empty` `wellFounded_lt` `Set.ext` `WellFounded.min_le` `WellFounded.min_mem`
`eq_univ_or_Ioi` 📖	mathematical	`IsUpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Set.univ` `Set.Ioi`	—	`IsLowerSet.eq_univ_or_Iio` `IsWellOrder.toIsWellFounded` `isWellOrder_lt` `instWellFoundedLTOrderDualOfWellFoundedGT`
`erase` 📖	mathematical	`IsUpperSet`	`Set` `Set.instSDiff` `Set.instSingletonSet`	—	`sdiff`
`image` 📖	mathematical	`IsUpperSet` `Preorder.toLE`	`Set.image` `DFunLike.coe` `OrderIso` `instFunLikeOrderIso`	—	`Equiv.image_eq_preimage_symm` `preimage` `OrderIso.monotone`
`inter` 📖	mathematical	`IsUpperSet`	`Set` `Set.instInter`	—	—
`isLowerSet_preimage_coe` 📖	mathematical	`IsUpperSet`	`IsLowerSet` `Set.Elem` `Set` `Set.instMembership` `Set.preimage`	—	—
`not_bddAbove` 📖	mathematical	`IsUpperSet` `Preorder.toLE` `Set.Nonempty`	`BddAbove`	—	`NoMaxOrder.exists_gt` `LT.lt.not_ge` `LE.le.trans` `LT.lt.le`
`ofDual` 📖	mathematical	`IsUpperSet` `OrderDual` `OrderDual.instLE`	`IsLowerSet` `Set.preimage` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	`isLowerSet_preimage_toDual_iff`
`ordConnected` 📖	mathematical	`IsUpperSet` `Preorder.toLE`	`Set.OrdConnected`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.Icc_subset_Ici_self` `Ici_subset`
`preimage` 📖	mathematical	`IsUpperSet` `Preorder.toLE` `Monotone`	`Set.preimage`	—	—
`sdiff` 📖	mathematical	`IsUpperSet` `Set` `Set.instMembership`	`Set.instSDiff`	—	—
`sdiff_of_isLowerSet` 📖	mathematical	`IsUpperSet` `IsLowerSet`	`Set` `Set.instSDiff`	—	`sdiff`
`toDual` 📖	mathematical	`IsUpperSet`	`IsLowerSet` `OrderDual` `OrderDual.instLE` `Set.preimage` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual`	—	`isLowerSet_preimage_ofDual_iff`
`top_mem` 📖	mathematical	`IsUpperSet` `Preorder.toLE`	`Set` `Set.instMembership` `Top.top` `OrderTop.toTop` `Set.Nonempty`	—	`le_top`
`top_notMem` 📖	mathematical	`IsUpperSet` `Preorder.toLE`	`Set` `Set.instMembership` `Top.top` `OrderTop.toTop` `Set.instEmptyCollection`	—	`Iff.not` `top_mem` `Set.not_nonempty_iff_eq_empty`
`total` 📖	mathematical	`IsUpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Set` `Set.instHasSubset`	—	`le_total`
`union` 📖	mathematical	`IsUpperSet`	`Set` `Set.instUnion`	—	—
`upperBounds_subset` 📖	mathematical	`IsUpperSet` `Preorder.toLE` `Set.Nonempty`	`Set` `Set.instHasSubset` `upperBounds`	—	—

OrderEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`image_Ici` 📖	mathematical	`IsUpperSet` `Preorder.toLE` `Set.range` `DFunLike.coe` `OrderEmbedding` `instFunLikeOrderEmbedding`	`Set.image` `Set.Ici`	—	`preimage_Ici` `Set.image_preimage_eq_inter_range` `Set.inter_eq_left` `IsUpperSet.Ici_subset` `Set.mem_range_self`
`image_Iic` 📖	mathematical	`IsLowerSet` `Preorder.toLE` `Set.range` `DFunLike.coe` `OrderEmbedding` `instFunLikeOrderEmbedding`	`Set.image` `Set.Iic`	—	`image_Ici`
`image_Iio` 📖	mathematical	`IsLowerSet` `Preorder.toLE` `Set.range` `DFunLike.coe` `OrderEmbedding` `instFunLikeOrderEmbedding`	`Set.image` `Set.Iio`	—	`image_Ioi`
`image_Ioi` 📖	mathematical	`IsUpperSet` `Preorder.toLE` `Set.range` `DFunLike.coe` `OrderEmbedding` `instFunLikeOrderEmbedding`	`Set.image` `Set.Ioi`	—	`preimage_Ioi` `Set.image_preimage_eq_inter_range` `Set.inter_eq_left` `IsUpperSet.Ioi_subset` `Set.mem_range_self`

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`antitone_mem` 📖	mathematical	—	`Antitone` `PartialOrder.toPreorder` `Prop.partialOrder` `Set` `instMembership` `IsLowerSet` `Preorder.toLE`	—	`forall_swap`
`monotone_mem` 📖	mathematical	—	`Monotone` `PartialOrder.toPreorder` `Prop.partialOrder` `Set` `instMembership` `IsUpperSet` `Preorder.toLE`	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLowerSet_Iic` 📖	mathematical	—	`IsLowerSet` `Preorder.toLE` `Set.Iic`	—	`le_trans`
`isLowerSet_Iio` 📖	mathematical	—	`IsLowerSet` `Preorder.toLE` `Set.Iio`	—	`lt_of_le_of_lt`
`isLowerSet_compl` 📖	mathematical	—	`IsLowerSet` `Compl.compl` `Set` `Set.instCompl` `IsUpperSet`	—	`compl_compl` `IsLowerSet.compl` `IsUpperSet.compl`
`isLowerSet_empty` 📖	mathematical	—	`IsLowerSet` `Set` `Set.instEmptyCollection`	—	—
`isLowerSet_iInter` 📖	mathematical	`IsLowerSet`	`Set.iInter`	—	`isLowerSet_sInter` `Set.forall_mem_range`
`isLowerSet_iInter₂` 📖	mathematical	`IsLowerSet`	`Set.iInter`	—	`isLowerSet_iInter`
`isLowerSet_iUnion` 📖	mathematical	`IsLowerSet`	`Set.iUnion`	—	`isLowerSet_sUnion` `Set.forall_mem_range`
`isLowerSet_iUnion₂` 📖	mathematical	`IsLowerSet`	`Set.iUnion`	—	`isLowerSet_iUnion`
`isLowerSet_iff_Iic_subset` 📖	mathematical	—	`IsLowerSet` `Preorder.toLE` `Set` `Set.instHasSubset` `Set.Iic`	—	`forall_swap`
`isLowerSet_iff_Iio_subset` 📖	mathematical	—	`IsLowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `Set` `Set.instHasSubset` `Set.Iio`	—	`forall_swap`
`isLowerSet_iff_forall_lt` 📖	mathematical	—	`IsLowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `Set` `Set.instMembership`	—	`le_iff_eq_or_lt'`
`isLowerSet_preimage_ofDual_iff` 📖	mathematical	—	`IsLowerSet` `OrderDual` `OrderDual.instLE` `Set.preimage` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual` `IsUpperSet`	—	—
`isLowerSet_preimage_toDual_iff` 📖	mathematical	—	`IsLowerSet` `Set.preimage` `OrderDual` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `IsUpperSet` `OrderDual.instLE`	—	—
`isLowerSet_sInter` 📖	mathematical	`IsLowerSet`	`Set.sInter`	—	`forall₂_imp`
`isLowerSet_sUnion` 📖	mathematical	`IsLowerSet`	`Set.sUnion`	—	—
`isLowerSet_setOf` 📖	mathematical	—	`IsLowerSet` `Preorder.toLE` `setOf` `Antitone` `PartialOrder.toPreorder` `Prop.partialOrder`	—	`forall_swap`
`isLowerSet_univ` 📖	mathematical	—	`IsLowerSet` `Set.univ`	—	—
`isUpperSet_Ici` 📖	mathematical	—	`IsUpperSet` `Preorder.toLE` `Set.Ici`	—	`ge_trans`
`isUpperSet_Ioi` 📖	mathematical	—	`IsUpperSet` `Preorder.toLE` `Set.Ioi`	—	`lt_of_lt_of_le`
`isUpperSet_compl` 📖	mathematical	—	`IsUpperSet` `Compl.compl` `Set` `Set.instCompl` `IsLowerSet`	—	`compl_compl` `IsUpperSet.compl` `IsLowerSet.compl`
`isUpperSet_empty` 📖	mathematical	—	`IsUpperSet` `Set` `Set.instEmptyCollection`	—	—
`isUpperSet_iInter` 📖	mathematical	`IsUpperSet`	`Set.iInter`	—	`isUpperSet_sInter` `Set.forall_mem_range`
`isUpperSet_iInter₂` 📖	mathematical	`IsUpperSet`	`Set.iInter`	—	`isUpperSet_iInter`
`isUpperSet_iUnion` 📖	mathematical	`IsUpperSet`	`Set.iUnion`	—	`isUpperSet_sUnion` `Set.forall_mem_range`
`isUpperSet_iUnion₂` 📖	mathematical	`IsUpperSet`	`Set.iUnion`	—	`isUpperSet_iUnion`
`isUpperSet_iff_Ici_subset` 📖	mathematical	—	`IsUpperSet` `Preorder.toLE` `Set` `Set.instHasSubset` `Set.Ici`	—	`forall_swap`
`isUpperSet_iff_Ioi_subset` 📖	mathematical	—	`IsUpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `Set` `Set.instHasSubset` `Set.Ioi`	—	`forall_swap`
`isUpperSet_iff_forall_lt` 📖	mathematical	—	`IsUpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `Set` `Set.instMembership`	—	—
`isUpperSet_preimage_ofDual_iff` 📖	mathematical	—	`IsUpperSet` `OrderDual` `OrderDual.instLE` `Set.preimage` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual` `IsLowerSet`	—	—
`isUpperSet_preimage_toDual_iff` 📖	mathematical	—	`IsUpperSet` `Set.preimage` `OrderDual` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `IsLowerSet` `OrderDual.instLE`	—	—
`isUpperSet_sInter` 📖	mathematical	`IsUpperSet`	`Set.sInter`	—	`forall₂_imp`
`isUpperSet_sUnion` 📖	mathematical	`IsUpperSet`	`Set.sUnion`	—	—
`isUpperSet_setOf` 📖	mathematical	—	`IsUpperSet` `Preorder.toLE` `setOf` `Monotone` `PartialOrder.toPreorder` `Prop.partialOrder`	—	—
`isUpperSet_univ` 📖	mathematical	—	`IsUpperSet` `Set.univ`	—	—
`not_bddAbove_Ici` 📖	mathematical	—	`BddAbove` `Preorder.toLE` `Set.Ici`	—	`IsUpperSet.not_bddAbove` `isUpperSet_Ici` `Set.nonempty_Ici`
`not_bddAbove_Ioi` 📖	mathematical	—	`BddAbove` `Preorder.toLE` `Set.Ioi`	—	`IsUpperSet.not_bddAbove` `isUpperSet_Ioi` `Set.nonempty_Ioi`
`not_bddBelow_Iic` 📖	mathematical	—	`BddBelow` `Preorder.toLE` `Set.Iic`	—	`IsLowerSet.not_bddBelow` `isLowerSet_Iic` `Set.nonempty_Iic`
`not_bddBelow_Iio` 📖	mathematical	—	`BddBelow` `Preorder.toLE` `Set.Iio`	—	`IsLowerSet.not_bddBelow` `isLowerSet_Iio` `Set.nonempty_Iio`

---

← Back to Index