UpperLower

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

Statistics

Metric	Count
Definitions `addCommSemigroup`, `commSemigroup`, `instAdd`, `instAddAction`, `instAddCommMonoid`, `instCommMonoid`, `instDiv`, `instMul`, `instMulAction`, `instOne`, `instSMul`, `instSub`, `instVAdd`, `instZero`, `addCommSemigroup`, `commSemigroup`, `instAdd`, `instAddAction`, `instAddCommMonoid`, `instCommMonoid`, `instDiv`, `instMul`, `instMulAction`, `instOne`, `instSMul`, `instSub`, `instVAdd`, `instZero`	28
Theorems `add_left`, `add_right`, `div_left`, `div_right`, `inv`, `mul_left`, `mul_right`, `neg`, `smul`, `smul_subset`, `sub_left`, `sub_right`, `vadd`, `vadd_subset`, `add_left`, `add_right`, `div_left`, `div_right`, `inv`, `mul_left`, `mul_right`, `neg`, `smul`, `smul_subset`, `sub_left`, `sub_right`, `vadd`, `vadd_subset`, `Iic_one`, `Iic_zero`, `coe_add`, `coe_div`, `coe_mul`, `coe_sub`, `smul`, `vadd`, `Ici_one`, `Ici_zero`, `coe_add`, `coe_div`, `coe_mul`, `coe_one`, `coe_sub`, `coe_zero`, `add_lowerClosure`, `add_upperClosure`, `lowerClosure_add`, `lowerClosure_add_distrib`, `lowerClosure_mul`, `lowerClosure_mul_distrib`, `lowerClosure_one`, `lowerClosure_smul`, `lowerClosure_vadd`, `lowerClosure_zero`, `mul_lowerClosure`, `mul_upperClosure`, `upperClosure_add`, `upperClosure_add_distrib`, `upperClosure_mul`, `upperClosure_mul_distrib`, `upperClosure_one`, `upperClosure_smul`, `upperClosure_vadd`, `upperClosure_zero`	64
Total	92

IsLowerSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_left` 📖	mathematical	`IsLowerSet` `Preorder.toLE` `PartialOrder.toPreorder`	`Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`IsUpperSet.add_left` `OrderDual.isOrderedAddMonoid` `AddCommGroup.add_comm` `toDual`
`add_right` 📖	mathematical	`IsLowerSet` `Preorder.toLE` `PartialOrder.toPreorder`	`Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`IsUpperSet.add_right` `OrderDual.isOrderedAddMonoid` `AddCommGroup.add_comm` `toDual`
`div_left` 📖	mathematical	`IsLowerSet` `Preorder.toLE` `PartialOrder.toPreorder`	`IsUpperSet` `Set` `Set.div` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup`	—	`IsUpperSet.div_left` `OrderDual.isOrderedMonoid` `CommGroup.mul_comm` `toDual`
`div_right` 📖	mathematical	`IsLowerSet` `Preorder.toLE` `PartialOrder.toPreorder`	`Set` `Set.div` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup`	—	`IsUpperSet.div_right` `OrderDual.isOrderedMonoid` `CommGroup.mul_comm` `toDual`
`inv` 📖	mathematical	`IsLowerSet` `Preorder.toLE` `PartialOrder.toPreorder`	`IsUpperSet` `Set` `Set.inv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid`	—	`inv_le_inv'`
`mul_left` 📖	mathematical	`IsLowerSet` `Preorder.toLE` `PartialOrder.toPreorder`	`Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup`	—	`IsUpperSet.mul_left` `OrderDual.isOrderedMonoid` `CommGroup.mul_comm` `toDual`
`mul_right` 📖	mathematical	`IsLowerSet` `Preorder.toLE` `PartialOrder.toPreorder`	`Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup`	—	`IsUpperSet.mul_right` `OrderDual.isOrderedMonoid` `CommGroup.mul_comm` `toDual`
`neg` 📖	mathematical	`IsLowerSet` `Preorder.toLE` `PartialOrder.toPreorder`	`IsUpperSet` `Set` `Set.neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`neg_le_neg`
`smul` 📖	mathematical	`IsLowerSet` `Preorder.toLE` `PartialOrder.toPreorder`	`Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `MulAction.toSemigroupAction` `Monoid.toMulAction`	—	`image` `IsOrderedMonoid.toMulLeftMono`
`smul_subset` 📖	mathematical	`IsLowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	`Set` `Set.instHasSubset` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Monoid.toMulAction`	—	`Set.smul_set_subset_iff` `mul_le_of_le_one_left'` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono`
`sub_left` 📖	mathematical	`IsLowerSet` `Preorder.toLE` `PartialOrder.toPreorder`	`IsUpperSet` `Set` `Set.sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`IsUpperSet.sub_left` `OrderDual.isOrderedAddMonoid` `AddCommGroup.add_comm` `toDual`
`sub_right` 📖	mathematical	`IsLowerSet` `Preorder.toLE` `PartialOrder.toPreorder`	`Set` `Set.sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`IsUpperSet.sub_right` `OrderDual.isOrderedAddMonoid` `AddCommGroup.add_comm` `toDual`
`vadd` 📖	mathematical	`IsLowerSet` `Preorder.toLE` `PartialOrder.toPreorder`	`HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction`	—	`image` `IsOrderedAddMonoid.toAddLeftMono`
`vadd_subset` 📖	mathematical	`IsLowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`Set` `Set.instHasSubset` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction`	—	`Set.vadd_set_subset_iff` `add_le_of_nonpos_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono`

IsUpperSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_left` 📖	mathematical	`IsUpperSet` `Preorder.toLE` `PartialOrder.toPreorder`	`Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`vadd_eq_add` `Set.iUnion_vadd_set` `isUpperSet_iUnion₂` `vadd`
`add_right` 📖	mathematical	`IsUpperSet` `Preorder.toLE` `PartialOrder.toPreorder`	`Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`add_comm` `add_left`
`div_left` 📖	mathematical	`IsUpperSet` `Preorder.toLE` `PartialOrder.toPreorder`	`IsLowerSet` `Set` `Set.div` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup`	—	`div_eq_mul_inv` `IsLowerSet.mul_left` `inv`
`div_right` 📖	mathematical	`IsUpperSet` `Preorder.toLE` `PartialOrder.toPreorder`	`Set` `Set.div` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup`	—	`div_eq_mul_inv` `mul_right`
`inv` 📖	mathematical	`IsUpperSet` `Preorder.toLE` `PartialOrder.toPreorder`	`IsLowerSet` `Set` `Set.inv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid`	—	`inv_le_inv'`
`mul_left` 📖	mathematical	`IsUpperSet` `Preorder.toLE` `PartialOrder.toPreorder`	`Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup`	—	`smul_eq_mul` `Set.iUnion_smul_set` `isUpperSet_iUnion₂` `smul`
`mul_right` 📖	mathematical	`IsUpperSet` `Preorder.toLE` `PartialOrder.toPreorder`	`Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup`	—	`mul_comm` `mul_left`
`neg` 📖	mathematical	`IsUpperSet` `Preorder.toLE` `PartialOrder.toPreorder`	`IsLowerSet` `Set` `Set.neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`neg_le_neg`
`smul` 📖	mathematical	`IsUpperSet` `Preorder.toLE` `PartialOrder.toPreorder`	`Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `MulAction.toSemigroupAction` `Monoid.toMulAction`	—	`image` `IsOrderedMonoid.toMulLeftMono`
`smul_subset` 📖	mathematical	`IsUpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	`Set` `Set.instHasSubset` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Monoid.toMulAction`	—	`Set.smul_set_subset_iff` `le_mul_of_one_le_left'` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono`
`sub_left` 📖	mathematical	`IsUpperSet` `Preorder.toLE` `PartialOrder.toPreorder`	`IsLowerSet` `Set` `Set.sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`sub_eq_add_neg` `IsLowerSet.add_left` `neg`
`sub_right` 📖	mathematical	`IsUpperSet` `Preorder.toLE` `PartialOrder.toPreorder`	`Set` `Set.sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`sub_eq_add_neg` `add_right`
`vadd` 📖	mathematical	`IsUpperSet` `Preorder.toLE` `PartialOrder.toPreorder`	`HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction`	—	`image` `IsOrderedAddMonoid.toAddLeftMono`
`vadd_subset` 📖	mathematical	`IsUpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`Set` `Set.instHasSubset` `HVAdd.hVAdd` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction`	—	`Set.vadd_set_subset_iff` `le_add_of_nonneg_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono`

LowerSet

Definitions

Name	Category	Theorems
`addCommSemigroup` 📖	CompOp	—
`commSemigroup` 📖	CompOp	—
`instAdd` 📖	CompOp	2 math math: `coe_add`, `lowerClosure_add_distrib`
`instAddAction` 📖	CompOp	—
`instAddCommMonoid` 📖	CompOp	—
`instCommMonoid` 📖	CompOp	—
`instDiv` 📖	CompOp	1 math math: `coe_div`
`instMul` 📖	CompOp	2 math math: `lowerClosure_mul_distrib`, `coe_mul`
`instMulAction` 📖	CompOp	—
`instOne` 📖	CompOp	2 math math: `lowerClosure_one`, `Iic_one`
`instSMul` 📖	CompOp	1 math math: `lowerClosure_smul`
`instSub` 📖	CompOp	1 math math: `coe_sub`
`instVAdd` 📖	CompOp	1 math math: `lowerClosure_vadd`
`instZero` 📖	CompOp	2 math math: `lowerClosure_zero`, `Iic_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Iic_one` 📖	mathematical	—	`Iic` `PartialOrder.toPreorder` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `LowerSet` `Preorder.toLE` `instOne`	—	—
`Iic_zero` 📖	mathematical	—	`Iic` `PartialOrder.toPreorder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `LowerSet` `Preorder.toLE` `instZero`	—	—
`coe_add` 📖	mathematical	—	`SetLike.coe` `LowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `instSetLike` `instAdd` `Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	—
`coe_div` 📖	mathematical	—	`SetLike.coe` `LowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `instSetLike` `instDiv` `Set` `Set.div` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup`	—	—
`coe_mul` 📖	mathematical	—	`SetLike.coe` `LowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `instSetLike` `instMul` `Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup`	—	—
`coe_sub` 📖	mathematical	—	`SetLike.coe` `LowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `instSetLike` `instSub` `Set` `Set.sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	—

Set.OrdConnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smul` 📖	mathematical	—	`Set.OrdConnected` `PartialOrder.toPreorder` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `MulAction.toSemigroupAction` `Monoid.toMulAction`	—	`upperClosure_inter_lowerClosure` `Set.smul_set_inter` `inter` `IsUpperSet.ordConnected` `IsUpperSet.smul` `UpperSet.upper` `IsLowerSet.ordConnected` `IsLowerSet.smul` `LowerSet.lower`
`vadd` 📖	mathematical	—	`Set.OrdConnected` `PartialOrder.toPreorder` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction`	—	`upperClosure_inter_lowerClosure` `Set.vadd_set_inter` `inter` `IsUpperSet.ordConnected` `IsUpperSet.vadd` `UpperSet.upper` `IsLowerSet.ordConnected` `IsLowerSet.vadd` `LowerSet.lower`

UpperSet

Definitions

Name	Category	Theorems
`addCommSemigroup` 📖	CompOp	—
`commSemigroup` 📖	CompOp	—
`instAdd` 📖	CompOp	2 math math: `coe_add`, `upperClosure_add_distrib`
`instAddAction` 📖	CompOp	—
`instAddCommMonoid` 📖	CompOp	—
`instCommMonoid` 📖	CompOp	—
`instDiv` 📖	CompOp	1 math math: `coe_div`
`instMul` 📖	CompOp	2 math math: `coe_mul`, `upperClosure_mul_distrib`
`instMulAction` 📖	CompOp	—
`instOne` 📖	CompOp	3 math math: `upperClosure_one`, `coe_one`, `Ici_one`
`instSMul` 📖	CompOp	1 math math: `upperClosure_smul`
`instSub` 📖	CompOp	1 math math: `coe_sub`
`instVAdd` 📖	CompOp	1 math math: `upperClosure_vadd`
`instZero` 📖	CompOp	3 math math: `upperClosure_zero`, `Ici_zero`, `coe_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Ici_one` 📖	mathematical	—	`Ici` `PartialOrder.toPreorder` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `UpperSet` `Preorder.toLE` `instOne`	—	—
`Ici_zero` 📖	mathematical	—	`Ici` `PartialOrder.toPreorder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `UpperSet` `Preorder.toLE` `instZero`	—	—
`coe_add` 📖	mathematical	—	`SetLike.coe` `UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `instSetLike` `instAdd` `Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	—
`coe_div` 📖	mathematical	—	`SetLike.coe` `UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `instSetLike` `instDiv` `Set` `Set.div` `DivInvMonoid.toDiv` `Group.toDivInvMonoid` `CommGroup.toGroup`	—	—
`coe_mul` 📖	mathematical	—	`SetLike.coe` `UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `instSetLike` `instMul` `Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup`	—	—
`coe_one` 📖	mathematical	—	`SetLike.coe` `UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `instSetLike` `instOne` `Set.Ici` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid`	—	—
`coe_sub` 📖	mathematical	—	`SetLike.coe` `UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `instSetLike` `instSub` `Set` `Set.sub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	—
`coe_zero` 📖	mathematical	—	`SetLike.coe` `UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `instSetLike` `instZero` `Set.Ici` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_lowerClosure` 📖	mathematical	—	`Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SetLike.coe` `LowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `LowerSet.instSetLike` `lowerClosure`	—	`Set.iUnion_vadd_set` `lowerClosure_iUnion` `iSup_congr_Prop` `lowerClosure_vadd` `LowerSet.coe_iSup₂`
`add_upperClosure` 📖	mathematical	—	`Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SetLike.coe` `UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `UpperSet.instSetLike` `upperClosure`	—	`Set.iUnion_vadd_set` `upperClosure_iUnion` `iInf_congr_Prop` `upperClosure_vadd` `UpperSet.coe_iInf₂`
`lowerClosure_add` 📖	mathematical	—	`Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SetLike.coe` `LowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `LowerSet.instSetLike` `lowerClosure`	—	`add_comm` `add_lowerClosure`
`lowerClosure_add_distrib` 📖	mathematical	—	`lowerClosure` `PartialOrder.toPreorder` `Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `LowerSet` `Preorder.toLE` `LowerSet.instAdd`	—	`SetLike.coe_injective` `LowerSet.coe_add` `add_lowerClosure` `lowerClosure_add` `LowerSet.lowerClosure`
`lowerClosure_mul` 📖	mathematical	—	`Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `SetLike.coe` `LowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `LowerSet.instSetLike` `lowerClosure`	—	`mul_comm` `mul_lowerClosure`
`lowerClosure_mul_distrib` 📖	mathematical	—	`lowerClosure` `PartialOrder.toPreorder` `Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `LowerSet` `Preorder.toLE` `LowerSet.instMul`	—	`SetLike.coe_injective` `LowerSet.coe_mul` `mul_lowerClosure` `lowerClosure_mul` `LowerSet.lowerClosure`
`lowerClosure_one` 📖	mathematical	—	`lowerClosure` `PartialOrder.toPreorder` `Set` `Set.one` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `LowerSet` `Preorder.toLE` `LowerSet.instOne`	—	`lowerClosure_singleton`
`lowerClosure_smul` 📖	mathematical	—	`lowerClosure` `PartialOrder.toPreorder` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `MulAction.toSemigroupAction` `Monoid.toMulAction` `LowerSet` `Preorder.toLE` `LowerSet.instSMul`	—	`lowerClosure_image` `IsOrderedMonoid.toMulLeftMono`
`lowerClosure_vadd` 📖	mathematical	—	`lowerClosure` `PartialOrder.toPreorder` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction` `LowerSet` `Preorder.toLE` `LowerSet.instVAdd`	—	`lowerClosure_image` `IsOrderedAddMonoid.toAddLeftMono`
`lowerClosure_zero` 📖	mathematical	—	`lowerClosure` `PartialOrder.toPreorder` `Set` `Set.zero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `LowerSet` `Preorder.toLE` `LowerSet.instZero`	—	`lowerClosure_singleton`
`mul_lowerClosure` 📖	mathematical	—	`Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `SetLike.coe` `LowerSet` `Preorder.toLE` `PartialOrder.toPreorder` `LowerSet.instSetLike` `lowerClosure`	—	`lowerClosure_iUnion` `iSup_congr_Prop` `lowerClosure_smul` `LowerSet.coe_iSup₂`
`mul_upperClosure` 📖	mathematical	—	`Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `SetLike.coe` `UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `UpperSet.instSetLike` `upperClosure`	—	`upperClosure_iUnion` `iInf_congr_Prop` `upperClosure_smul` `UpperSet.coe_iInf₂`
`upperClosure_add` 📖	mathematical	—	`Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `SetLike.coe` `UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `UpperSet.instSetLike` `upperClosure`	—	`add_comm` `add_upperClosure`
`upperClosure_add_distrib` 📖	mathematical	—	`upperClosure` `PartialOrder.toPreorder` `Set` `Set.add` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `UpperSet` `Preorder.toLE` `UpperSet.instAdd`	—	`SetLike.coe_injective` `UpperSet.coe_add` `add_upperClosure` `upperClosure_add` `UpperSet.upperClosure`
`upperClosure_mul` 📖	mathematical	—	`Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `SetLike.coe` `UpperSet` `Preorder.toLE` `PartialOrder.toPreorder` `UpperSet.instSetLike` `upperClosure`	—	`mul_comm` `mul_upperClosure`
`upperClosure_mul_distrib` 📖	mathematical	—	`upperClosure` `PartialOrder.toPreorder` `Set` `Set.mul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `UpperSet` `Preorder.toLE` `UpperSet.instMul`	—	`SetLike.coe_injective` `UpperSet.coe_mul` `mul_upperClosure` `upperClosure_mul` `UpperSet.upperClosure`
`upperClosure_one` 📖	mathematical	—	`upperClosure` `PartialOrder.toPreorder` `Set` `Set.one` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroup.toDivisionCommMonoid` `UpperSet` `Preorder.toLE` `UpperSet.instOne`	—	`upperClosure_singleton`
`upperClosure_smul` 📖	mathematical	—	`upperClosure` `PartialOrder.toPreorder` `Set` `Set.smulSet` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `MulAction.toSemigroupAction` `Monoid.toMulAction` `UpperSet` `Preorder.toLE` `UpperSet.instSMul`	—	`upperClosure_image` `IsOrderedMonoid.toMulLeftMono`
`upperClosure_vadd` 📖	mathematical	—	`upperClosure` `PartialOrder.toPreorder` `HVAdd.hVAdd` `Set` `instHVAdd` `Set.vaddSet` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddMonoid.toAddAction` `UpperSet` `Preorder.toLE` `UpperSet.instVAdd`	—	`upperClosure_image` `IsOrderedAddMonoid.toAddLeftMono`
`upperClosure_zero` 📖	mathematical	—	`upperClosure` `PartialOrder.toPreorder` `Set` `Set.zero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `UpperSet` `Preorder.toLE` `UpperSet.instZero`	—	`upperClosure_singleton`

---

← Back to Index