ExtrClosure

📁 Source: Mathlib/Topology/Order/ExtrClosure.lean

Statistics

Metric	Count
Definitions	0
Theorems closure, closure, closure, closure, closure, closure	6
Total	6

IsExtrOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure 📖	—	IsExtrOn ContinuousOn closure	—	—	elim IsMinOn.closure IsMaxOn.closure

IsLocalExtrOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure 📖	—	IsLocalExtrOn ContinuousOn closure	—	—	elim IsLocalMinOn.closure IsLocalMaxOn.closure

IsLocalMaxOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure 📖	—	IsLocalMaxOn ContinuousOn closure	—	—	mem_nhdsWithin ContinuousWithinAt.closure_le mem_closure_iff_nhdsWithin_neBot nhdsWithin_inter_of_mem nhdsWithin_le_nhds IsOpen.mem_nhds ContinuousWithinAt.mono HasSubset.Subset.trans Set.instIsTransSubset Set.inter_subset_right subset_closure continuousWithinAt_const

IsLocalMinOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure 📖	—	IsLocalMinOn ContinuousOn closure	—	—	IsLocalMaxOn.closure instOrderClosedTopologyOrderDual IsMinFilter.dual

IsMaxOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure 📖	—	IsMaxOn ContinuousOn closure	—	—	ContinuousWithinAt.closure_le ContinuousWithinAt.mono subset_closure continuousWithinAt_const

IsMinOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure 📖	—	IsMinOn ContinuousOn closure	—	—	IsMaxOn.closure instOrderClosedTopologyOrderDual dual

---

← Back to Index