UpperLower

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

Statistics

Metric	Count
Definitions HasUpperLowerClosure	1
Theorems isLowerSet_closure, isOpen_lowerClosure, isOpen_upperClosure, isUpperSet_closure, closure, interior, lowerClosure, upperClosure, to_hasUpperLowerClosure, to_hasUpperLowerClosure, closure, interior, interior, instHasUpperLowerClosureOrderDual	14
Total	15

HasUpperLowerClosure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLowerSet_closure 📖	mathematical	IsLowerSet Preorder.toLE	closure	—	—
isOpen_lowerClosure 📖	mathematical	IsOpen	SetLike.coe LowerSet Preorder.toLE LowerSet.instSetLike lowerClosure	—	—
isOpen_upperClosure 📖	mathematical	IsOpen	SetLike.coe UpperSet Preorder.toLE UpperSet.instSetLike upperClosure	—	—
isUpperSet_closure 📖	mathematical	IsUpperSet Preorder.toLE	closure	—	—

IsLowerSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure 📖	mathematical	IsLowerSet Preorder.toLE	closure	—	HasUpperLowerClosure.isLowerSet_closure
interior 📖	mathematical	IsLowerSet Preorder.toLE	interior	—	IsUpperSet.interior instHasUpperLowerClosureOrderDual toDual

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lowerClosure 📖	mathematical	IsOpen	SetLike.coe LowerSet Preorder.toLE LowerSet.instSetLike lowerClosure	—	HasUpperLowerClosure.isOpen_lowerClosure
upperClosure 📖	mathematical	IsOpen	SetLike.coe UpperSet Preorder.toLE UpperSet.instSetLike upperClosure	—	HasUpperLowerClosure.isOpen_upperClosure

IsOrderedAddMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
to_hasUpperLowerClosure 📖	mathematical	—	HasUpperLowerClosure PartialOrder.toPreorder	—	closure_mono IsUpperSet.vadd_subset sub_nonneg covariant_swap_add_of_covariant_add toAddLeftMono closure_vadd sub_add_cancel IsLowerSet.vadd_subset sub_nonpos add_zero add_upperClosure IsOpen.add_right ContinuousConstVAdd.op AddCommSemigroup.isCentralVAdd add_lowerClosure

IsOrderedMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
to_hasUpperLowerClosure 📖	mathematical	—	HasUpperLowerClosure PartialOrder.toPreorder	—	closure_mono IsUpperSet.smul_subset one_le_div' covariant_swap_mul_of_covariant_mul toMulLeftMono closure_smul div_mul_cancel IsLowerSet.smul_subset div_le_one' mul_one mul_upperClosure IsOpen.mul_right ContinuousConstSMul.op CommSemigroup.isCentralScalar mul_lowerClosure

IsUpperSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure 📖	mathematical	IsUpperSet Preorder.toLE	closure	—	HasUpperLowerClosure.isUpperSet_closure
interior 📖	mathematical	IsUpperSet Preorder.toLE	interior	—	isLowerSet_compl closure_compl IsLowerSet.closure compl

Set.OrdConnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
interior 📖	mathematical	—	Set.OrdConnected interior	—	upperClosure_inter_lowerClosure interior_inter inter IsUpperSet.ordConnected IsUpperSet.interior UpperSet.upper IsLowerSet.ordConnected IsLowerSet.interior LowerSet.lower

(root)

Definitions

Name	Category	Theorems
HasUpperLowerClosure 📖	CompData	3 math math: IsOrderedMonoid.to_hasUpperLowerClosure, IsOrderedAddMonoid.to_hasUpperLowerClosure, instHasUpperLowerClosureOrderDual

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasUpperLowerClosureOrderDual 📖	mathematical	—	HasUpperLowerClosure OrderDual OrderDual.instTopologicalSpace OrderDual.instPreorder	—	IsLowerSet.closure IsUpperSet.closure IsOpen.lowerClosure IsOpen.upperClosure

---

← Back to Index