OrderClosedExtr

Statistics

Metric	Count
Definitions	0
Theorems `isLocalMax_of_mono_anti`, `isLocalMin_of_anti_mono`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`isLocalMax_of_mono_anti` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MonotoneOn` `Set.Ioc` `AntitoneOn` `Set.Ico`	`IsLocalMax`	—	`isLocalMax_of_mono_anti'` `Ioc_mem_nhdsLE` `instClosedIicTopology` `Ico_mem_nhdsGE` `instClosedIciTopology`
`isLocalMin_of_anti_mono` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AntitoneOn` `Set.Ioc` `MonotoneOn` `Set.Ico`	`IsLocalMin`	—	`Filter.mem_of_superset` `Ioo_mem_nhds` `le_total`

---