Prod

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

Statistics

Metric	Count
Definitions `instSProd`, `prod`, `instSProd`, `prod`	4
Theorems `prod`, `prod`, `Ici_prod_Ici`, `Iic_prod`, `bot_prod`, `coe_prod`, `disjoint_prod`, `inf_prod`, `mem_prod`, `prod_bot`, `prod_eq_bot`, `prod_inf`, `prod_inf_prod`, `prod_le_prod_iff`, `prod_mono`, `prod_mono_left`, `prod_mono_right`, `prod_self_le_prod_self`, `prod_self_lt_prod_self`, `prod_sup`, `sup_prod`, `top_prod_top`, `Ici_prod`, `Ici_prod_Ici`, `bot_prod_bot`, `codisjoint_prod`, `coe_prod`, `inf_prod`, `mem_prod`, `prod_eq_top`, `prod_inf`, `prod_le_prod_iff`, `prod_mono`, `prod_mono_left`, `prod_mono_right`, `prod_self_le_prod_self`, `prod_self_lt_prod_self`, `prod_sup`, `prod_sup_prod`, `prod_top`, `sup_prod`, `top_prod`, `lowerClosure_prod`, `upperClosure_prod`	44
Total	48

IsLowerSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod` 📖	mathematical	`IsLowerSet` `Preorder.toLE`	`Prod.instLE_mathlib` `SProd.sprod` `Set` `Set.instSProd`	—	—

IsUpperSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod` 📖	mathematical	`IsUpperSet` `Preorder.toLE`	`Prod.instLE_mathlib` `SProd.sprod` `Set` `Set.instSProd`	—	—

LowerSet

Definitions

Name	Category	Theorems
`instSProd` 📖	CompOp	21 math math: `inf_prod`, `sup_prod`, `prod_mono`, `prod_self_lt_prod_self`, `bot_prod`, `lowerClosure_prod`, `prod_mono_left`, `disjoint_prod`, `top_prod_top`, `coe_prod`, `prod_mono_right`, `prod_self_le_prod_self`, `prod_eq_bot`, `prod_sup`, `prod_le_prod_iff`, `prod_bot`, `prod_inf_prod`, `Iic_prod`, `prod_inf`, `mem_prod`, `Ici_prod_Ici`
`prod` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Ici_prod_Ici` 📖	mathematical	—	`SProd.sprod` `LowerSet` `Preorder.toLE` `Prod.instLE_mathlib` `instSProd` `Iic` `Prod.instPreorder`	—	—
`Iic_prod` 📖	mathematical	—	`Iic` `Prod.instPreorder` `SProd.sprod` `LowerSet` `Preorder.toLE` `Prod.instLE_mathlib` `instSProd`	—	—
`bot_prod` 📖	mathematical	—	`SProd.sprod` `LowerSet` `Preorder.toLE` `Prod.instLE_mathlib` `instSProd` `Bot.bot` `instBot`	—	`ext` `Set.empty_prod`
`coe_prod` 📖	mathematical	—	`SetLike.coe` `LowerSet` `Prod.instLE_mathlib` `Preorder.toLE` `instSetLike` `SProd.sprod` `instSProd` `Set` `Set.instSProd`	—	—
`disjoint_prod` 📖	mathematical	—	`Disjoint` `LowerSet` `Prod.instLE_mathlib` `Preorder.toLE` `instPartialOrder` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompletelyDistribLattice.toCompleteDistribLattice` `completelyDistribLattice` `SProd.sprod` `instSProd`	—	`prod_inf_prod`
`inf_prod` 📖	mathematical	—	`SProd.sprod` `LowerSet` `Preorder.toLE` `Prod.instLE_mathlib` `instSProd` `instMin`	—	`ext` `Set.inter_prod`
`mem_prod` 📖	mathematical	—	`LowerSet` `Prod.instLE_mathlib` `Preorder.toLE` `SetLike.instMembership` `instSetLike` `SProd.sprod` `instSProd`	—	—
`prod_bot` 📖	mathematical	—	`SProd.sprod` `LowerSet` `Preorder.toLE` `Prod.instLE_mathlib` `instSProd` `Bot.bot` `instBot`	—	`ext` `Set.prod_empty`
`prod_eq_bot` 📖	mathematical	—	`SProd.sprod` `LowerSet` `Preorder.toLE` `Prod.instLE_mathlib` `instSProd` `Bot.bot` `instBot`	—	`Set.prod_eq_empty_iff`
`prod_inf` 📖	mathematical	—	`SProd.sprod` `LowerSet` `Preorder.toLE` `Prod.instLE_mathlib` `instSProd` `instMin`	—	`ext` `Set.prod_inter`
`prod_inf_prod` 📖	mathematical	—	`LowerSet` `Prod.instLE_mathlib` `Preorder.toLE` `instMin` `SProd.sprod` `instSProd`	—	`ext` `Set.prod_inter_prod`
`prod_le_prod_iff` 📖	mathematical	—	`LowerSet` `Prod.instLE_mathlib` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `SProd.sprod` `instSProd` `Bot.bot` `instBot`	—	`Set.prod_subset_prod_iff` `instIsConcreteLE`
`prod_mono` 📖	mathematical	`LowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Prod.instLE_mathlib` `SProd.sprod` `instSProd`	—	`Set.prod_mono`
`prod_mono_left` 📖	mathematical	`LowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Prod.instLE_mathlib` `SProd.sprod` `instSProd`	—	`Set.prod_mono_left`
`prod_mono_right` 📖	mathematical	`LowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Prod.instLE_mathlib` `SProd.sprod` `instSProd`	—	`Set.prod_mono_right`
`prod_self_le_prod_self` 📖	mathematical	—	`LowerSet` `Prod.instLE_mathlib` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `SProd.sprod` `instSProd`	—	`Set.prod_self_subset_prod_self`
`prod_self_lt_prod_self` 📖	mathematical	—	`LowerSet` `Prod.instLE_mathlib` `Preorder.toLE` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `SProd.sprod` `instSProd`	—	`Set.prod_self_ssubset_prod_self`
`prod_sup` 📖	mathematical	—	`SProd.sprod` `LowerSet` `Preorder.toLE` `Prod.instLE_mathlib` `instSProd` `instMax`	—	`ext` `Set.prod_union`
`sup_prod` 📖	mathematical	—	`SProd.sprod` `LowerSet` `Preorder.toLE` `Prod.instLE_mathlib` `instSProd` `instMax`	—	`ext` `Set.union_prod`
`top_prod_top` 📖	mathematical	—	`SProd.sprod` `LowerSet` `Preorder.toLE` `Prod.instLE_mathlib` `instSProd` `Top.top` `instTop`	—	`ext` `Set.univ_prod_univ`

UpperSet

Definitions

Name	Category	Theorems
`instSProd` 📖	CompOp	21 math math: `prod_le_prod_iff`, `coe_prod`, `prod_top`, `top_prod`, `Ici_prod_Ici`, `prod_mono_left`, `sup_prod`, `upperClosure_prod`, `prod_inf`, `prod_mono`, `prod_self_le_prod_self`, `prod_self_lt_prod_self`, `mem_prod`, `bot_prod_bot`, `prod_sup_prod`, `prod_mono_right`, `codisjoint_prod`, `inf_prod`, `prod_eq_top`, `Ici_prod`, `prod_sup`
`prod` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Ici_prod` 📖	mathematical	—	`Ici` `Prod.instPreorder` `SProd.sprod` `UpperSet` `Preorder.toLE` `Prod.instLE_mathlib` `instSProd`	—	—
`Ici_prod_Ici` 📖	mathematical	—	`SProd.sprod` `UpperSet` `Preorder.toLE` `Prod.instLE_mathlib` `instSProd` `Ici` `Prod.instPreorder`	—	—
`bot_prod_bot` 📖	mathematical	—	`SProd.sprod` `UpperSet` `Preorder.toLE` `Prod.instLE_mathlib` `instSProd` `Bot.bot` `instBot`	—	`ext` `Set.univ_prod_univ`
`codisjoint_prod` 📖	mathematical	—	`Codisjoint` `UpperSet` `Prod.instLE_mathlib` `Preorder.toLE` `instPartialOrder` `CoheytingAlgebra.toOrderTop` `Order.Coframe.toCoheytingAlgebra` `CompleteDistribLattice.toCoframe` `CompletelyDistribLattice.toCompleteDistribLattice` `completelyDistribLattice` `SProd.sprod` `instSProd`	—	`prod_sup_prod`
`coe_prod` 📖	mathematical	—	`SetLike.coe` `UpperSet` `Prod.instLE_mathlib` `Preorder.toLE` `instSetLike` `SProd.sprod` `instSProd` `Set` `Set.instSProd`	—	—
`inf_prod` 📖	mathematical	—	`SProd.sprod` `UpperSet` `Preorder.toLE` `Prod.instLE_mathlib` `instSProd` `instMin`	—	`ext` `Set.union_prod`
`mem_prod` 📖	mathematical	—	`UpperSet` `Prod.instLE_mathlib` `Preorder.toLE` `SetLike.instMembership` `instSetLike` `SProd.sprod` `instSProd`	—	—
`prod_eq_top` 📖	mathematical	—	`SProd.sprod` `UpperSet` `Preorder.toLE` `Prod.instLE_mathlib` `instSProd` `Top.top` `instTop`	—	`Set.prod_eq_empty_iff`
`prod_inf` 📖	mathematical	—	`SProd.sprod` `UpperSet` `Preorder.toLE` `Prod.instLE_mathlib` `instSProd` `instMin`	—	`ext` `Set.prod_union`
`prod_le_prod_iff` 📖	mathematical	—	`UpperSet` `Prod.instLE_mathlib` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `SProd.sprod` `instSProd` `Top.top` `instTop`	—	`Set.prod_subset_prod_iff`
`prod_mono` 📖	mathematical	`UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Prod.instLE_mathlib` `SProd.sprod` `instSProd`	—	`Set.prod_mono`
`prod_mono_left` 📖	mathematical	`UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Prod.instLE_mathlib` `SProd.sprod` `instSProd`	—	`Set.prod_mono_left`
`prod_mono_right` 📖	mathematical	`UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Prod.instLE_mathlib` `SProd.sprod` `instSProd`	—	`Set.prod_mono_right`
`prod_self_le_prod_self` 📖	mathematical	—	`UpperSet` `Prod.instLE_mathlib` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `SProd.sprod` `instSProd`	—	`Set.prod_self_subset_prod_self`
`prod_self_lt_prod_self` 📖	mathematical	—	`UpperSet` `Prod.instLE_mathlib` `Preorder.toLE` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `SProd.sprod` `instSProd`	—	`Set.prod_self_ssubset_prod_self`
`prod_sup` 📖	mathematical	—	`SProd.sprod` `UpperSet` `Preorder.toLE` `Prod.instLE_mathlib` `instSProd` `instMax`	—	`ext` `Set.prod_inter`
`prod_sup_prod` 📖	mathematical	—	`UpperSet` `Prod.instLE_mathlib` `Preorder.toLE` `instMax` `SProd.sprod` `instSProd`	—	`ext` `Set.prod_inter_prod`
`prod_top` 📖	mathematical	—	`SProd.sprod` `UpperSet` `Preorder.toLE` `Prod.instLE_mathlib` `instSProd` `Top.top` `instTop`	—	`ext` `Set.prod_empty`
`sup_prod` 📖	mathematical	—	`SProd.sprod` `UpperSet` `Preorder.toLE` `Prod.instLE_mathlib` `instSProd` `instMax`	—	`ext` `Set.inter_prod`
`top_prod` 📖	mathematical	—	`SProd.sprod` `UpperSet` `Preorder.toLE` `Prod.instLE_mathlib` `instSProd` `Top.top` `instTop`	—	`ext` `Set.empty_prod`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lowerClosure_prod` 📖	mathematical	—	`lowerClosure` `Prod.instPreorder` `SProd.sprod` `Set` `Set.instSProd` `LowerSet` `Preorder.toLE` `Prod.instLE_mathlib` `LowerSet.instSProd`	—	`LowerSet.ext` `Set.ext`
`upperClosure_prod` 📖	mathematical	—	`upperClosure` `Prod.instPreorder` `SProd.sprod` `Set` `Set.instSProd` `UpperSet` `Preorder.toLE` `Prod.instLE_mathlib` `UpperSet.instSProd`	—	`UpperSet.ext` `Set.ext`

---

← Back to Index