Basic

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

Statistics

Metric	Count
Definitions `boundedOrder`, `coeHom`, `completeLattice`, `dual`, `instCoeNonemptyInterval`, `instInhabited`, `instLE`, `instOrderBot`, `instPreorder`, `instUniqueOfIsEmpty`, `lattice`, `map`, `partialOrder`, `pure`, `recBotCoe`, `semilatticeSup`, `setLike`, `NonemptyInterval`, `coeHom`, `dual`, `instCoeSet`, `instDecidableEq`, `instDecidableLE`, `instDecidableLE_1`, `instInhabited`, `instMax`, `instMembership`, `instOrderTop`, `instPartialOrder`, `instPreorder`, `instSemilatticeSup`, `le`, `map`, `map₂`, `pure`, `setLike`, `toDualProd`, `toDualProdHom`, `toProd`	39
Theorems `bot_ne_pure`, `canLift`, `coe_bot`, `coe_coe`, `coe_dual`, `coe_iInf`, `coe_iInf₂`, `coe_inf`, `coe_inj`, `coe_injective`, `coe_pure`, `coe_sInf`, `coe_sSubset_coe`, `coe_subset_coe`, `coe_top`, `disjoint_coe`, `dual_bot`, `dual_map`, `dual_pure`, `dual_top`, `exists`, `forall`, `instNontrivialOfNonempty`, `map_map`, `map_pure`, `mem_pure`, `mem_pure_self`, `pure_injective`, `pure_ne_bot`, `subset_coe_map`, `coe_coeHom`, `coe_def`, `coe_dual`, `coe_eq_pure`, `coe_nonempty`, `coe_pure`, `coe_pure_interval`, `coe_ssubset_coe`, `coe_subset_coe`, `coe_sup_interval`, `coe_top`, `coe_top_interval`, `dual_map`, `dual_map₂`, `dual_pure`, `dual_top`, `ext`, `ext_iff`, `fst_dual`, `fst_le_snd`, `fst_sup`, `instCanLift`, `instIsEmpty`, `instNonempty`, `instNontrivial`, `instSubsingleton`, `le_def`, `map_fst`, `map_map`, `map_pure`, `map_snd`, `map₂_fst`, `map₂_pure`, `map₂_snd`, `mem_coe_interval`, `mem_def`, `mem_mk`, `mem_pure`, `mem_pure_self`, `pure_fst`, `pure_injective`, `pure_snd`, `snd_dual`, `snd_sup`, `subset_coe_map`, `toDualProdHom_apply`, `toDualProd_apply`, `toDualProd_injective`, `toDualProd_mono`, `toDualProd_strictMono`, `toProd_injective`	81
Total	120

Interval

Definitions

Name	Category	Theorems
`boundedOrder` 📖	CompOp	—
`coeHom` 📖	CompOp	—
`completeLattice` 📖	CompOp	3 math math: `coe_sInf`, `coe_iInf₂`, `coe_iInf`
`dual` 📖	CompOp	5 math math: `coe_dual`, `dual_top`, `dual_bot`, `dual_pure`, `dual_map`
`instCoeNonemptyInterval` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`instLE` 📖	CompOp	1 math math: `coe_subset_coe`
`instOrderBot` 📖	CompOp	1 math math: `disjoint_coe`
`instPreorder` 📖	CompOp	1 math math: `coe_sSubset_coe`
`instUniqueOfIsEmpty` 📖	CompOp	—
`lattice` 📖	CompOp	1 math math: `coe_inf`
`map` 📖	CompOp	4 math math: `subset_coe_map`, `map_pure`, `dual_map`, `map_map`
`partialOrder` 📖	CompOp	1 math math: `disjoint_coe`
`pure` 📖	CompOp	13 math math: `mem_pure`, `pure_zero`, `add_eq_zero_iff`, `pure_injective`, `dual_pure`, `map_pure`, `NonemptyInterval.coe_eq_pure`, `pure_one`, `mul_eq_one_iff`, `NonemptyInterval.coe_pure_interval`, `length_pure`, `coe_pure`, `mem_pure_self`
`recBotCoe` 📖	CompOp	—
`semilatticeSup` 📖	CompOp	1 math math: `NonemptyInterval.coe_sup_interval`
`setLike` 📖	CompOp	20 math math: `NonemptyInterval.mem_coe_interval`, `coe_sInf`, `coe_iInf₂`, `mem_pure`, `one_mem_one`, `coe_dual`, `subset_coe_map`, `coe_zero`, `coe_iInf`, `coe_coe`, `coe_top`, `coe_one`, `disjoint_coe`, `coe_subset_coe`, `coe_sSubset_coe`, `coe_bot`, `zero_mem_zero`, `coe_inf`, `coe_pure`, `mem_pure_self`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_ne_pure` 📖	—	—	—	—	`WithBot.bot_ne_coe`
`canLift` 📖	mathematical	—	`CanLift` `Interval` `NonemptyInterval` `WithBot.some` `Bot.bot` `WithBot.bot`	—	`WithBot.canLift`
`coe_bot` 📖	mathematical	—	`SetLike.coe` `Interval` `Preorder.toLE` `PartialOrder.toPreorder` `setLike` `Bot.bot` `WithBot.bot` `NonemptyInterval` `Set` `Set.instEmptyCollection`	—	—
`coe_coe` 📖	mathematical	—	`SetLike.coe` `WithBot` `NonemptyInterval` `Preorder.toLE` `PartialOrder.toPreorder` `setLike` `WithBot.some` `NonemptyInterval.setLike`	—	—
`coe_dual` 📖	mathematical	—	`SetLike.coe` `Interval` `OrderDual` `OrderDual.instLE` `Preorder.toLE` `PartialOrder.toPreorder` `setLike` `OrderDual.instPartialOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `dual` `Set.preimage` `OrderDual.ofDual`	—	`NonemptyInterval.coe_dual`
`coe_iInf` 📖	mathematical	—	`SetLike.coe` `Interval` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `setLike` `iInf` `CompleteSemilatticeInf.toInfSet` `completeLattice` `Set.iInter`	—	`coe_sInf` `Set.iInter_congr_Prop` `Set.iInter_exists` `Set.iInter_iInter_eq'`
`coe_iInf₂` 📖	mathematical	—	`SetLike.coe` `Interval` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `setLike` `iInf` `CompleteSemilatticeInf.toInfSet` `completeLattice` `Set.iInter`	—	`coe_iInf`
`coe_inf` 📖	mathematical	—	`SetLike.coe` `Interval` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `setLike` `SemilatticeInf.toMin` `lattice` `Set` `Set.instInter`	—	`bot_inf_eq` `Set.empty_inter` `inf_bot_eq` `Set.inter_empty` `Set.Icc_inter_Icc` `Set.Icc_eq_empty` `LE.le.trans` `le_sup_left` `inf_le_right` `le_sup_right` `inf_le_left`
`coe_inj` 📖	mathematical	—	`WithBot.some` `NonemptyInterval`	—	—
`coe_injective` 📖	mathematical	—	`NonemptyInterval` `WithBot` `WithBot.some`	—	`WithBot.coe_injective`
`coe_pure` 📖	mathematical	—	`SetLike.coe` `Interval` `Preorder.toLE` `PartialOrder.toPreorder` `setLike` `pure` `Set` `Set.instSingletonSet`	—	`Set.Icc_self`
`coe_sInf` 📖	mathematical	—	`SetLike.coe` `Interval` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `setLike` `InfSet.sInf` `CompleteSemilatticeInf.toInfSet` `completeLattice` `Set.iInter` `Set` `Set.instMembership`	—	`Set.ext` `instIsEmptyFalse` `Set.eq_empty_of_subset_empty` `Set.iInter₂_subset_of_subset` `Set.Subset.rfl` `Set.not_nonempty_iff_eq_empty` `LE.le.trans` `Set.mem_iInter₂`
`coe_sSubset_coe` 📖	mathematical	—	`Set` `Set.instHasSSubset` `SetLike.coe` `Interval` `Preorder.toLE` `PartialOrder.toPreorder` `setLike` `Preorder.toLT` `instPreorder`	—	`OrderEmbedding.lt_iff_lt`
`coe_subset_coe` 📖	mathematical	—	`Set` `Set.instHasSubset` `SetLike.coe` `Interval` `Preorder.toLE` `PartialOrder.toPreorder` `setLike` `instLE`	—	`OrderEmbedding.le_iff_le`
`coe_top` 📖	mathematical	—	`SetLike.coe` `Interval` `Preorder.toLE` `PartialOrder.toPreorder` `setLike` `Top.top` `WithBot.instTop` `NonemptyInterval` `OrderTop.toTop` `NonemptyInterval.le` `NonemptyInterval.instOrderTop` `Set.univ`	—	`Set.Icc_bot_top`
`disjoint_coe` 📖	mathematical	—	`Disjoint` `Set` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `SetLike.coe` `Interval` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `setLike` `partialOrder` `instOrderBot`	—	`disjoint_iff_inf_le` `coe_subset_coe` `coe_inf`
`dual_bot` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Interval` `Preorder.toLE` `OrderDual` `OrderDual.instLE` `EquivLike.toFunLike` `Equiv.instEquivLike` `dual` `Bot.bot` `WithBot.bot` `NonemptyInterval`	—	—
`dual_map` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Interval` `Preorder.toLE` `OrderDual` `OrderDual.instLE` `EquivLike.toFunLike` `Equiv.instEquivLike` `dual` `map` `OrderDual.instPreorder` `OrderHom` `OrderHom.dual`	—	`WithBot.map_comm`
`dual_pure` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Interval` `Preorder.toLE` `OrderDual` `OrderDual.instLE` `EquivLike.toFunLike` `Equiv.instEquivLike` `dual` `pure` `OrderDual.instPreorder` `OrderDual.toDual`	—	—
`dual_top` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Interval` `Preorder.toLE` `OrderDual` `OrderDual.instLE` `EquivLike.toFunLike` `Equiv.instEquivLike` `dual` `Top.top` `WithBot.instTop` `NonemptyInterval` `OrderTop.toTop` `NonemptyInterval.le` `NonemptyInterval.instOrderTop` `OrderDual.instPreorder` `OrderDual.instBoundedOrder`	—	—
`exists` 📖	mathematical	—	`Bot.bot` `Interval` `WithBot.bot` `NonemptyInterval` `WithBot.some`	—	—
`forall` 📖	mathematical	—	`Bot.bot` `Interval` `WithBot.bot` `NonemptyInterval` `WithBot.some`	—	—
`instNontrivialOfNonempty` 📖	mathematical	—	`Nontrivial` `Interval` `Preorder.toLE`	—	`Option.nontrivial` `NonemptyInterval.instNonempty`
`map_map` 📖	mathematical	—	`map` `OrderHom.comp`	—	—
`map_pure` 📖	mathematical	—	`map` `pure` `DFunLike.coe` `OrderHom` `OrderHom.instFunLike`	—	—
`mem_pure` 📖	mathematical	—	`Interval` `Preorder.toLE` `PartialOrder.toPreorder` `SetLike.instMembership` `setLike` `pure`	—	`SetLike.mem_coe` `coe_pure` `Set.mem_singleton_iff`
`mem_pure_self` 📖	mathematical	—	`Interval` `Preorder.toLE` `PartialOrder.toPreorder` `SetLike.instMembership` `setLike` `pure`	—	`mem_pure`
`pure_injective` 📖	mathematical	—	`Interval` `Preorder.toLE` `pure`	—	`coe_injective` `NonemptyInterval.pure_injective`
`pure_ne_bot` 📖	—	—	—	—	`WithBot.coe_ne_bot`
`subset_coe_map` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.image` `DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `OrderHom.instFunLike` `SetLike.coe` `Interval` `Preorder.toLE` `setLike` `map`	—	`Set.image_empty` `NonemptyInterval.subset_coe_map`

NonemptyInterval

Definitions

Name	Category	Theorems
`coeHom` 📖	CompOp	1 math math: `coe_coeHom`
`dual` 📖	CompOp	7 math math: `dual_map`, `coe_dual`, `dual_top`, `dual_pure`, `fst_dual`, `dual_map₂`, `snd_dual`
`instCoeSet` 📖	CompOp	—
`instDecidableEq` 📖	CompOp	—
`instDecidableLE` 📖	CompOp	—
`instDecidableLE_1` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`instMax` 📖	CompOp	3 math math: `snd_sup`, `fst_sup`, `coe_sup_interval`
`instMembership` 📖	CompOp	7 math math: `mem_coe_interval`, `mem_mk`, `mem_pure`, `mem_pure_self`, `one_mem_one`, `mem_def`, `zero_mem_zero`
`instOrderTop` 📖	CompOp	5 math math: `dual_top`, `Interval.dual_top`, `coe_top_interval`, `Interval.coe_top`, `coe_top`
`instPartialOrder` 📖	CompOp	—
`instPreorder` 📖	CompOp	5 math math: `toDualProd_mono`, `toLex_strictMono`, `coe_ssubset_coe`, `toDualProd_strictMono`, `toLex_mono`
`instSemilatticeSup` 📖	CompOp	—
`le` 📖	CompOp	9 math math: `dual_top`, `toDualProdHom_apply`, `Interval.dual_top`, `coe_subset_coe`, `coe_top_interval`, `Interval.coe_top`, `coe_coeHom`, `le_def`, `coe_top`
`map` 📖	CompOp	6 math math: `dual_map`, `map_pure`, `map_snd`, `map_fst`, `subset_coe_map`, `map_map`
`map₂` 📖	CompOp	4 math math: `map₂_snd`, `dual_map₂`, `map₂_fst`, `map₂_pure`
`pure` 📖	CompOp	25 math math: `pure_fst`, `pure_pow`, `map_pure`, `mem_pure`, `mem_pure_self`, `pure_mul_pure`, `add_eq_zero_iff`, `pure_sub_pure`, `dual_pure`, `pure_add_pure`, `pure_nsmul`, `pure_injective`, `pure_div_pure`, `pure_natCast`, `coe_eq_pure`, `pure_one`, `length_pure`, `pure_zero`, `neg_pure`, `pure_snd`, `coe_pure`, `coe_pure_interval`, `map₂_pure`, `inv_pure`, `mul_eq_one_iff`
`setLike` 📖	CompOp	11 math math: `coe_dual`, `coe_zero`, `coe_ssubset_coe`, `coe_subset_coe`, `coe_one`, `Interval.coe_coe`, `coe_coeHom`, `coe_def`, `subset_coe_map`, `coe_pure`, `coe_top`
`toDualProd` 📖	CompOp	5 math math: `toDualProd_mono`, `toDualProdHom_apply`, `toDualProd_strictMono`, `toDualProd_apply`, `toDualProd_injective`
`toDualProdHom` 📖	CompOp	1 math math: `toDualProdHom_apply`
`toProd` 📖	CompOp	49 math math: `pure_fst`, `fst_add`, `snd_neg`, `snd_zero`, `snd_div`, `toProd_nsmul`, `snd_add`, `snd_inv`, `fst_sub`, `toProd_injective`, `map₂_snd`, `toProd_one`, `toProd_pow`, `fst_dual`, `toProd_zero`, `fst_inv`, `coe_nonempty`, `map₂_fst`, `snd_sub`, `fst_div`, `fst_natCast`, `ext_iff`, `map_snd`, `snd_one`, `snd_sup`, `fst_zero`, `instCanLift`, `fst_one`, `fst_nsmul`, `fst_neg`, `fst_mul`, `toProd_mul`, `coe_def`, `map_fst`, `mem_def`, `snd_mul`, `snd_natCast`, `toLex_lt_toLex`, `fst_sup`, `le_def`, `pure_snd`, `snd_dual`, `snd_pow`, `toDualProd_apply`, `snd_nsmul`, `fst_le_snd`, `fst_pow`, `toLex_le_toLex`, `toProd_add`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_coeHom` 📖	mathematical	—	`DFunLike.coe` `OrderEmbedding` `NonemptyInterval` `Preorder.toLE` `PartialOrder.toPreorder` `Set` `le` `Set.instLE` `instFunLikeOrderEmbedding` `coeHom` `SetLike.coe` `setLike`	—	—
`coe_def` 📖	mathematical	—	`SetLike.coe` `NonemptyInterval` `Preorder.toLE` `PartialOrder.toPreorder` `setLike` `Set.Icc` `toProd`	—	—
`coe_dual` 📖	mathematical	—	`SetLike.coe` `NonemptyInterval` `OrderDual` `OrderDual.instLE` `Preorder.toLE` `PartialOrder.toPreorder` `setLike` `OrderDual.instPartialOrder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `dual` `Set.preimage` `OrderDual.ofDual`	—	`Set.Icc_toDual`
`coe_eq_pure` 📖	mathematical	—	`WithBot.some` `NonemptyInterval` `Preorder.toLE` `Interval.pure` `pure`	—	`coe_pure_interval`
`coe_nonempty` 📖	mathematical	—	`Set.Nonempty` `Set.Icc` `toProd` `Preorder.toLE`	—	`Set.nonempty_Icc` `fst_le_snd`
`coe_pure` 📖	mathematical	—	`SetLike.coe` `NonemptyInterval` `Preorder.toLE` `PartialOrder.toPreorder` `setLike` `pure` `Set` `Set.instSingletonSet`	—	`Set.Icc_self`
`coe_pure_interval` 📖	mathematical	—	`WithBot.some` `NonemptyInterval` `Preorder.toLE` `pure` `Interval.pure`	—	—
`coe_ssubset_coe` 📖	mathematical	—	`Set` `Set.instHasSSubset` `SetLike.coe` `NonemptyInterval` `Preorder.toLE` `PartialOrder.toPreorder` `setLike` `Preorder.toLT` `instPreorder`	—	`OrderEmbedding.lt_iff_lt`
`coe_subset_coe` 📖	mathematical	—	`Set` `Set.instHasSubset` `SetLike.coe` `NonemptyInterval` `Preorder.toLE` `PartialOrder.toPreorder` `setLike` `le`	—	`OrderEmbedding.le_iff_le`
`coe_sup_interval` 📖	mathematical	—	`WithBot.some` `NonemptyInterval` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instMax` `WithBot` `SemilatticeSup.toMax` `Interval.semilatticeSup`	—	—
`coe_top` 📖	mathematical	—	`SetLike.coe` `NonemptyInterval` `Preorder.toLE` `PartialOrder.toPreorder` `setLike` `Top.top` `OrderTop.toTop` `le` `instOrderTop` `Set.univ`	—	`Set.Icc_bot_top`
`coe_top_interval` 📖	mathematical	—	`WithBot.some` `NonemptyInterval` `Preorder.toLE` `Top.top` `OrderTop.toTop` `le` `instOrderTop` `WithBot` `WithBot.instTop`	—	—
`dual_map` 📖	mathematical	—	`DFunLike.coe` `Equiv` `NonemptyInterval` `Preorder.toLE` `OrderDual` `OrderDual.instLE` `EquivLike.toFunLike` `Equiv.instEquivLike` `dual` `map` `OrderDual.instPreorder` `OrderHom` `OrderHom.dual`	—	—
`dual_map₂` 📖	mathematical	`Monotone`	`DFunLike.coe` `Equiv` `NonemptyInterval` `Preorder.toLE` `OrderDual` `OrderDual.instLE` `EquivLike.toFunLike` `Equiv.instEquivLike` `dual` `map₂` `OrderDual.instPreorder` `OrderDual.toDual` `OrderDual.ofDual` `Monotone.dual`	—	—
`dual_pure` 📖	mathematical	—	`DFunLike.coe` `Equiv` `NonemptyInterval` `Preorder.toLE` `OrderDual` `OrderDual.instLE` `EquivLike.toFunLike` `Equiv.instEquivLike` `dual` `pure` `OrderDual.instPreorder` `OrderDual.toDual`	—	—
`dual_top` 📖	mathematical	—	`DFunLike.coe` `Equiv` `NonemptyInterval` `Preorder.toLE` `OrderDual` `OrderDual.instLE` `EquivLike.toFunLike` `Equiv.instEquivLike` `dual` `Top.top` `OrderTop.toTop` `le` `instOrderTop` `OrderDual.instPreorder` `OrderDual.instBoundedOrder`	—	—
`ext` 📖	—	`toProd`	—	—	—
`ext_iff` 📖	mathematical	—	`toProd`	—	`ext`
`fst_dual` 📖	mathematical	—	`OrderDual` `toProd` `OrderDual.instLE` `DFunLike.coe` `Equiv` `NonemptyInterval` `EquivLike.toFunLike` `Equiv.instEquivLike` `dual` `OrderDual.toDual`	—	—
`fst_le_snd` 📖	mathematical	—	`toProd`	—	—
`fst_sup` 📖	mathematical	—	`toProd` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `NonemptyInterval` `instMax` `SemilatticeInf.toMin`	—	—
`instCanLift` 📖	mathematical	—	`CanLift` `NonemptyInterval` `toProd`	—	—
`instIsEmpty` 📖	mathematical	—	`IsEmpty` `NonemptyInterval`	—	—
`instNonempty` 📖	mathematical	—	`NonemptyInterval` `Preorder.toLE`	—	`Nonempty.map`
`instNontrivial` 📖	mathematical	—	`Nontrivial` `NonemptyInterval` `Preorder.toLE`	—	`Function.Injective.nontrivial` `pure_injective`
`instSubsingleton` 📖	mathematical	—	`NonemptyInterval`	—	`Function.Injective.subsingleton` `toDualProd_injective` `OrderDual.instSubsingleton`
`le_def` 📖	mathematical	—	`NonemptyInterval` `le` `toProd`	—	—
`map_fst` 📖	mathematical	—	`toProd` `Preorder.toLE` `map` `DFunLike.coe` `OrderHom` `OrderHom.instFunLike`	—	—
`map_map` 📖	mathematical	—	`map` `OrderHom.comp`	—	—
`map_pure` 📖	mathematical	—	`map` `pure` `DFunLike.coe` `OrderHom` `OrderHom.instFunLike`	—	—
`map_snd` 📖	mathematical	—	`toProd` `Preorder.toLE` `map` `DFunLike.coe` `OrderHom` `OrderHom.instFunLike`	—	—
`map₂_fst` 📖	mathematical	`Monotone`	`toProd` `Preorder.toLE` `map₂`	—	—
`map₂_pure` 📖	mathematical	`Monotone`	`map₂` `pure`	—	—
`map₂_snd` 📖	mathematical	`Monotone`	`toProd` `Preorder.toLE` `map₂`	—	—
`mem_coe_interval` 📖	mathematical	—	`WithBot` `NonemptyInterval` `Preorder.toLE` `PartialOrder.toPreorder` `SetLike.instMembership` `Interval.setLike` `WithBot.some` `instMembership`	—	—
`mem_def` 📖	mathematical	—	`NonemptyInterval` `Preorder.toLE` `instMembership` `toProd`	—	—
`mem_mk` 📖	mathematical	`Preorder.toLE`	`NonemptyInterval` `instMembership`	—	—
`mem_pure` 📖	mathematical	—	`NonemptyInterval` `Preorder.toLE` `PartialOrder.toPreorder` `instMembership` `pure`	—	`SetLike.mem_coe` `coe_pure` `Set.mem_singleton_iff`
`mem_pure_self` 📖	mathematical	—	`NonemptyInterval` `Preorder.toLE` `instMembership` `pure`	—	`le_rfl`
`pure_fst` 📖	mathematical	—	`toProd` `Preorder.toLE` `pure`	—	—
`pure_injective` 📖	mathematical	—	`NonemptyInterval` `Preorder.toLE` `pure`	—	—
`pure_snd` 📖	mathematical	—	`toProd` `Preorder.toLE` `pure`	—	—
`snd_dual` 📖	mathematical	—	`OrderDual` `toProd` `OrderDual.instLE` `DFunLike.coe` `Equiv` `NonemptyInterval` `EquivLike.toFunLike` `Equiv.instEquivLike` `dual` `OrderDual.toDual`	—	—
`snd_sup` 📖	mathematical	—	`toProd` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `NonemptyInterval` `instMax` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	—
`subset_coe_map` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.image` `DFunLike.coe` `OrderHom` `PartialOrder.toPreorder` `OrderHom.instFunLike` `SetLike.coe` `NonemptyInterval` `Preorder.toLE` `setLike` `map`	—	`Set.image_subset_iff` `OrderHom.mono`
`toDualProdHom_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `NonemptyInterval` `OrderDual` `le` `Prod.instLE_mathlib` `OrderDual.instLE` `RelEmbedding.instFunLike` `toDualProdHom` `toDualProd`	—	—
`toDualProd_apply` 📖	mathematical	—	`toDualProd` `OrderDual` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `toProd`	—	—
`toDualProd_injective` 📖	mathematical	—	`NonemptyInterval` `OrderDual` `toDualProd`	—	`toProd_injective`
`toDualProd_mono` 📖	mathematical	—	`Monotone` `NonemptyInterval` `Preorder.toLE` `OrderDual` `instPreorder` `Prod.instPreorder` `OrderDual.instPreorder` `toDualProd`	—	—
`toDualProd_strictMono` 📖	mathematical	—	`StrictMono` `NonemptyInterval` `Preorder.toLE` `OrderDual` `instPreorder` `Prod.instPreorder` `OrderDual.instPreorder` `toDualProd`	—	—
`toProd_injective` 📖	mathematical	—	`NonemptyInterval` `toProd`	—	—

(root)

Definitions

Name	Category	Theorems
`NonemptyInterval` 📖	CompData	132 math math: `NonemptyInterval.toDualProd_mono`, `NonemptyInterval.dual_map`, `NonemptyInterval.length_zero`, `NonemptyInterval.pure_pow`, `NonemptyInterval.mem_coe_interval`, `NonemptyInterval.coe_inv_interval`, `NonemptyInterval.fst_add`, `NonemptyInterval.snd_neg`, `NonemptyInterval.instIsEmpty`, `Interval.div_bot`, `NonemptyInterval.coe_neg_interval`, `NonemptyInterval.snd_zero`, `NonemptyInterval.mem_mk`, `NonemptyInterval.mem_pure`, `NonemptyInterval.snd_div`, `NonemptyInterval.mem_pure_self`, `NonemptyInterval.pure_mul_pure`, `NonemptyInterval.toProd_nsmul`, `Interval.bot_add`, `NonemptyInterval.add_eq_zero_iff`, `NonemptyInterval.toLex_strictMono`, `NonemptyInterval.coe_dual`, `NonemptyInterval.coe_sub_interval`, `NonemptyInterval.coe_one_interval`, `NonemptyInterval.snd_add`, `NonemptyInterval.snd_inv`, `NonemptyInterval.fst_sub`, `NonemptyInterval.instSubsingleton`, `NonemptyInterval.dual_top`, `NonemptyInterval.toProd_injective`, `NonemptyInterval.pure_sub_pure`, `NonemptyInterval.coe_nsmul_interval`, `NonemptyInterval.toDualProdHom_apply`, `NonemptyInterval.toProd_one`, `NonemptyInterval.toProd_pow`, `NonemptyInterval.coe_pow_interval`, `NonemptyInterval.coe_add_interval`, `NonemptyInterval.dual_pure`, `Interval.one_mem_one`, `NonemptyInterval.fst_dual`, `NonemptyInterval.coe_div_interval`, `NonemptyInterval.coe_zero`, `Interval.dual_top`, `Interval.bot_mul`, `Interval.coe_zero`, `NonemptyInterval.toProd_zero`, `NonemptyInterval.fst_inv`, `Interval.pure_zero`, `NonemptyInterval.pure_add_pure`, `NonemptyInterval.pure_nsmul`, `NonemptyInterval.coe_ssubset_coe`, `NonemptyInterval.toDualProd_strictMono`, `Interval.add_eq_zero_iff`, `NonemptyInterval.coe_subset_coe`, `Interval.coe_injective`, `Interval.dual_bot`, `NonemptyInterval.dual_map₂`, `NonemptyInterval.coe_one`, `Interval.canLift`, `NonemptyInterval.snd_sub`, `NonemptyInterval.fst_div`, `NonemptyInterval.coe_top_interval`, `NonemptyInterval.fst_natCast`, `NonemptyInterval.one_mem_one`, `Interval.neg_bot`, `Interval.coe_coe`, `Interval.sub_bot`, `Interval.add_bot`, `NonemptyInterval.snd_one`, `NonemptyInterval.snd_sup`, `Interval.coe_top`, `Interval.coe_one`, `Interval.mul_bot`, `NonemptyInterval.length_add`, `NonemptyInterval.fst_zero`, `Interval.forall`, `Interval.bot_div`, `NonemptyInterval.pure_injective`, `Interval.coe_inj`, `NonemptyInterval.instCanLift`, `NonemptyInterval.pure_div_pure`, `NonemptyInterval.fst_one`, `NonemptyInterval.fst_nsmul`, `NonemptyInterval.length_sum`, `NonemptyInterval.fst_neg`, `NonemptyInterval.fst_mul`, `Interval.length_zero`, `NonemptyInterval.toProd_mul`, `NonemptyInterval.coe_coeHom`, `NonemptyInterval.coe_def`, `NonemptyInterval.length_sub`, `Interval.coe_bot`, `NonemptyInterval.coe_zero_interval`, `NonemptyInterval.pure_natCast`, `NonemptyInterval.mem_def`, `NonemptyInterval.zero_mem_zero`, `Interval.inv_bot`, `NonemptyInterval.coe_eq_pure`, `NonemptyInterval.pure_one`, `NonemptyInterval.instNonempty`, `Interval.bot_sub`, `Interval.pure_one`, `NonemptyInterval.subset_coe_map`, `NonemptyInterval.snd_mul`, `Interval.zero_mem_zero`, `NonemptyInterval.toLex_mono`, `NonemptyInterval.pure_zero`, `NonemptyInterval.snd_natCast`, `Interval.mul_eq_one_iff`, `NonemptyInterval.toLex_lt_toLex`, `NonemptyInterval.fst_sup`, `NonemptyInterval.neg_pure`, `NonemptyInterval.le_def`, `NonemptyInterval.coe_sup_interval`, `Interval.exists`, `NonemptyInterval.coe_pure`, `Interval.bot_pow`, `NonemptyInterval.coe_pure_interval`, `NonemptyInterval.snd_dual`, `NonemptyInterval.snd_pow`, `Interval.bot_nsmul`, `NonemptyInterval.toDualProd_injective`, `NonemptyInterval.snd_nsmul`, `NonemptyInterval.coe_top`, `NonemptyInterval.coe_mul_interval`, `NonemptyInterval.instNontrivial`, `NonemptyInterval.inv_pure`, `NonemptyInterval.fst_pow`, `NonemptyInterval.toLex_le_toLex`, `NonemptyInterval.length_neg`, `NonemptyInterval.mul_eq_one_iff`, `NonemptyInterval.toProd_add`

---

← Back to Index