Principal

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

Statistics

Metric	Count
Definitions `Iic`, `Iio`, `Ici`, `Ioi`	4
Theorems `Iic_iInf`, `Iic_iInf₂`, `Iic_inf`, `Iic_inj`, `Iic_injective`, `Iic_le`, `Iic_ne_Iic`, `Iic_ne_bot`, `Iic_sInf`, `Iic_strictMono`, `Iic_top`, `Iio_bot`, `Iio_eq_bot`, `Iio_strictMono`, `Ioi_le_Ici`, `bot_lt_Iic`, `coe_Iic`, `coe_Iio`, `map_Iic`, `map_Iio`, `mem_Iic_iff`, `mem_Iio_iff`, `Ici_bot`, `Ici_iSup`, `Ici_iSup₂`, `Ici_inj`, `Ici_injective`, `Ici_le_Ioi`, `Ici_lt_top`, `Ici_ne_Ici`, `Ici_ne_top`, `Ici_sSup`, `Ici_strictMono`, `Ici_sup`, `Ioi_eq_top`, `Ioi_strictMono`, `Ioi_top`, `coe_Ici`, `coe_Ioi`, `le_Ici`, `map_Ici`, `map_Ioi`, `mem_Ici_iff`, `mem_Ioi_iff`	44
Total	48

LowerSet

Definitions

Name	Category	Theorems
`Iic` 📖	CompOp	31 math math: `iSup_Iic`, `OrderEmbedding.supIrredLowerSet_apply`, `Iic_inj`, `Iic_top`, `lowerClosure_singleton`, `bot_lt_Iic`, `Iic_sup_erase`, `Iic_iInf`, `Order.Ideal.principal_toLowerSet`, `Iic_one`, `Iic_injective`, `coe_iicsInfHom`, `supIrred_iff_of_finite`, `iicsInfHom_apply`, `erase_sup_Iic`, `Iic_strictMono`, `OrderIso.supIrredLowerSet_apply`, `Iic_iInf₂`, `Iic_le`, `coe_Iic`, `iicInfHom_apply`, `mem_Iic_iff`, `Iic_sInf`, `coe_iicInfHom`, `Iic_prod`, `map_Iic`, `Iic_inf`, `supIrred_Iic`, `Iic_zero`, `UpperSet.coe_erase`, `Ici_prod_Ici`
`Iio` 📖	CompOp	6 math math: `map_Iio`, `Iio_strictMono`, `Iio_bot`, `coe_Iio`, `Iio_eq_bot`, `mem_Iio_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Iic_iInf` 📖	mathematical	—	`Iic` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `iInf` `CompleteSemilatticeInf.toInfSet` `LowerSet` `Preorder.toLE` `instInfSet`	—	`SetLike.ext`
`Iic_iInf₂` 📖	mathematical	—	`Iic` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `iInf` `CompleteSemilatticeInf.toInfSet` `LowerSet` `Preorder.toLE` `instInfSet`	—	`Iic_iInf`
`Iic_inf` 📖	mathematical	—	`Iic` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `SemilatticeInf.toMin` `LowerSet` `Preorder.toLE` `instMin`	—	`SetLike.coe_injective` `Set.Iic_inter_Iic`
`Iic_inj` 📖	mathematical	—	`Iic` `PartialOrder.toPreorder`	—	`Iic_injective`
`Iic_injective` 📖	mathematical	—	`LowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `Iic`	—	`Set.Iic_injective`
`Iic_le` 📖	mathematical	—	`LowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Iic` `SetLike.instMembership` `instSetLike`	—	`le_rfl` `IsLowerSet.Iic_subset` `lower`
`Iic_ne_Iic` 📖	—	—	—	—	`Iff.not`
`Iic_ne_bot` 📖	—	—	—	—	`SetLike.coe_ne_coe` `Set.Nonempty.ne_empty` `Set.nonempty_Iic`
`Iic_sInf` 📖	mathematical	—	`Iic` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `InfSet.sInf` `CompleteSemilatticeInf.toInfSet` `iInf` `LowerSet` `Preorder.toLE` `instInfSet` `Set` `Set.instMembership`	—	`SetLike.ext`
`Iic_strictMono` 📖	mathematical	—	`StrictMono` `LowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Iic`	—	`Set.Iic_ssubset_Iic`
`Iic_top` 📖	mathematical	—	`Iic` `Top.top` `OrderTop.toTop` `Preorder.toLE` `LowerSet` `instTop`	—	`SetLike.coe_injective` `Set.Iic_top`
`Iio_bot` 📖	mathematical	—	`Iio` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `LowerSet` `instBot`	—	`SetLike.coe_injective` `Set.Iio_bot`
`Iio_eq_bot` 📖	mathematical	—	`Iio` `PartialOrder.toPreorder` `Bot.bot` `LowerSet` `Preorder.toLE` `instBot` `OrderBot.toBot`	—	—
`Iio_strictMono` 📖	mathematical	—	`StrictMono` `LowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Iio`	—	`Set.Iio_ssubset_Iio`
`Ioi_le_Ici` 📖	mathematical	—	`Set` `Set.instLE` `Set.Ioi` `Set.Ici`	—	`Set.Ioi_subset_Ici_self`
`bot_lt_Iic` 📖	mathematical	—	`LowerSet` `Preorder.toLE` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `Bot.bot` `instBot` `Iic`	—	`bot_lt_iff_ne_bot` `Iic_ne_bot`
`coe_Iic` 📖	mathematical	—	`SetLike.coe` `LowerSet` `Preorder.toLE` `instSetLike` `Iic` `Set.Iic`	—	—
`coe_Iio` 📖	mathematical	—	`SetLike.coe` `LowerSet` `Preorder.toLE` `instSetLike` `Iio` `Set.Iio`	—	—
`map_Iic` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `LowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instFunLikeOrderIso` `map` `Iic`	—	`ext` `Set.ext` `OrderIso.image_Iic`
`map_Iio` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `LowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instFunLikeOrderIso` `map` `Iio`	—	`ext` `Set.ext` `OrderIso.image_Iio`
`mem_Iic_iff` 📖	mathematical	—	`LowerSet` `Preorder.toLE` `SetLike.instMembership` `instSetLike` `Iic`	—	—
`mem_Iio_iff` 📖	mathematical	—	`LowerSet` `Preorder.toLE` `SetLike.instMembership` `instSetLike` `Iio` `Preorder.toLT`	—	—

UpperSet

Definitions

Name	Category	Theorems
`Ici` 📖	CompOp	31 math math: `coe_Ici`, `Ici_injective`, `Ici_inf_erase`, `Ici_zero`, `Ici_lt_top`, `Ici_iSup`, `upperClosure_singleton`, `Ici_sup`, `Ici_sSup`, `mem_Ici_iff`, `OrderEmbedding.infIrredUpperSet_apply`, `Ici_prod_Ici`, `coe_iciSupHom`, `infIrred_Ici`, `le_Ici`, `erase_inf_Ici`, `LowerSet.coe_erase`, `map_Ici`, `coe_icisSupHom`, `Ici_one`, `icisSupHom_apply`, `iciSupHom_apply`, `OrderIso.infIrredUpperSet_apply`, `infIrred_iff_of_finite`, `Ici_le_Ioi`, `Ici_bot`, `Ici_inj`, `Ici_prod`, `iInf_Ici`, `Ici_iSup₂`, `Ici_strictMono`
`Ioi` 📖	CompOp	7 math math: `mem_Ioi_iff`, `Ioi_top`, `Ioi_eq_top`, `map_Ioi`, `Ioi_strictMono`, `coe_Ioi`, `Ici_le_Ioi`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Ici_bot` 📖	mathematical	—	`Ici` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `UpperSet` `instBot`	—	`SetLike.coe_injective` `Set.Ici_bot`
`Ici_iSup` 📖	mathematical	—	`Ici` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `UpperSet` `Preorder.toLE` `instSupSet`	—	`SetLike.ext`
`Ici_iSup₂` 📖	mathematical	—	`Ici` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `UpperSet` `Preorder.toLE` `instSupSet`	—	`Ici_iSup`
`Ici_inj` 📖	mathematical	—	`Ici` `PartialOrder.toPreorder`	—	`Ici_injective`
`Ici_injective` 📖	mathematical	—	`UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `Ici`	—	`Set.Ici_injective`
`Ici_le_Ioi` 📖	mathematical	—	`UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Ici` `Ioi`	—	`Set.Ioi_subset_Ici_self`
`Ici_lt_top` 📖	mathematical	—	`UpperSet` `Preorder.toLE` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `Ici` `Top.top` `instTop`	—	`lt_top_iff_ne_top` `Ici_ne_top`
`Ici_ne_Ici` 📖	—	—	—	—	`Iff.not`
`Ici_ne_top` 📖	—	—	—	—	`SetLike.coe_ne_coe` `Set.Nonempty.ne_empty` `Set.nonempty_Ici`
`Ici_sSup` 📖	mathematical	—	`Ici` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `SupSet.sSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `iSup` `UpperSet` `Preorder.toLE` `instSupSet` `Set` `Set.instMembership`	—	`SetLike.ext`
`Ici_strictMono` 📖	mathematical	—	`StrictMono` `UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Ici`	—	`Set.Ici_ssubset_Ici`
`Ici_sup` 📖	mathematical	—	`Ici` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SemilatticeSup.toMax` `UpperSet` `Preorder.toLE` `instMax`	—	`ext` `Set.Ici_inter_Ici`
`Ioi_eq_top` 📖	mathematical	—	`Ioi` `PartialOrder.toPreorder` `Top.top` `UpperSet` `Preorder.toLE` `instTop` `OrderTop.toTop`	—	—
`Ioi_strictMono` 📖	mathematical	—	`StrictMono` `UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Ioi`	—	`Set.Ioi_ssubset_Ioi`
`Ioi_top` 📖	mathematical	—	`Ioi` `Top.top` `OrderTop.toTop` `Preorder.toLE` `UpperSet` `instTop`	—	`SetLike.coe_injective` `Set.Ioi_top`
`coe_Ici` 📖	mathematical	—	`SetLike.coe` `UpperSet` `Preorder.toLE` `instSetLike` `Ici` `Set.Ici`	—	—
`coe_Ioi` 📖	mathematical	—	`SetLike.coe` `UpperSet` `Preorder.toLE` `instSetLike` `Ioi` `Set.Ioi`	—	—
`le_Ici` 📖	mathematical	—	`UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Ici` `SetLike.instMembership` `instSetLike`	—	`le_rfl` `IsUpperSet.Ici_subset` `upper`
`map_Ici` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instFunLikeOrderIso` `map` `Ici`	—	`ext` `Set.ext` `OrderIso.image_Ici`
`map_Ioi` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instFunLikeOrderIso` `map` `Ioi`	—	`ext` `Set.ext` `OrderIso.image_Ioi`
`mem_Ici_iff` 📖	mathematical	—	`UpperSet` `Preorder.toLE` `SetLike.instMembership` `instSetLike` `Ici`	—	—
`mem_Ioi_iff` 📖	mathematical	—	`UpperSet` `Preorder.toLE` `SetLike.instMembership` `instSetLike` `Ioi` `Preorder.toLT`	—	—

---

← Back to Index