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 📖	mathematical	IsExtrOn ContinuousOn closure	IsExtrOn closure	—	elim IsMinOn.closure IsMaxOn.closure

IsLocalExtrOn

Theorems

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

IsLocalMaxOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure 📖	mathematical	IsLocalMaxOn ContinuousOn closure	IsLocalMaxOn 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 📖	mathematical	IsLocalMinOn ContinuousOn closure	IsLocalMinOn closure	—	IsLocalMaxOn.closure instOrderClosedTopologyOrderDual IsMinFilter.dual

IsMaxOn

Theorems

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

IsMinOn

Theorems

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

---

← Back to Index