Documentation Verification Report

LocalExtr

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

Statistics

Metric	Count
Definitions `IsLocalExtr`, `IsLocalExtrOn`, `IsLocalMax`, `IsLocalMaxOn`, `IsLocalMin`, `IsLocalMinOn`	6
Theorems `isLocalExtrOn_iff`, `isLocalExtr_iff`, `isLocalMaxOn_iff`, `isLocalMax_iff`, `isLocalMinOn_iff`, `isLocalMin_iff`, `isLocalMax`, `isLocalMaxOn`, `isLocalMin`, `isLocalMinOn`, `isLocalExtr`, `localize`, `comp_antitone`, `comp_continuous`, `comp_continuousOn`, `comp_mono`, `elim`, `neg`, `on`, `comp_antitone`, `comp_continuousOn`, `comp_mono`, `elim`, `inter`, `isLocalExtr`, `neg`, `not_nhds_le_map`, `on_subset`, `add`, `bicomp_mono`, `comp_antitone`, `comp_continuous`, `comp_continuousOn`, `comp_mono`, `inf`, `max`, `min`, `neg`, `on`, `sub`, `sup`, `add`, `bicomp_mono`, `comp_antitone`, `comp_continuousOn`, `comp_mono`, `inf`, `inter`, `isLocalMax`, `max`, `min`, `neg`, `not_nhds_le_map`, `on_subset`, `sub`, `sup`, `add`, `bicomp_mono`, `comp_antitone`, `comp_continuous`, `comp_continuousOn`, `comp_mono`, `inf`, `max`, `min`, `neg`, `on`, `sub`, `sup`, `add`, `bicomp_mono`, `comp_antitone`, `comp_continuousOn`, `comp_mono`, `inf`, `inter`, `isLocalMin`, `max`, `min`, `neg`, `not_nhds_le_map`, `on_subset`, `sub`, `sup`, `isLocalMax`, `localize`, `isLocalMin`, `localize`, `isLocalExtrOn_const`, `isLocalExtrOn_univ_iff`, `isLocalExtr_const`, `isLocalMaxOn_const`, `isLocalMaxOn_univ_iff`, `isLocalMax_const`, `isLocalMax_of_mono_anti'`, `isLocalMinOn_const`, `isLocalMinOn_univ_iff`, `isLocalMin_const`, `isLocalMin_of_anti_mono'`	99
Total	105

Filter.EventuallyEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLocalExtrOn_iff` 📖	mathematical	`Filter.EventuallyEq` `nhdsWithin` `Set` `Set.instMembership`	`IsLocalExtrOn`	—	`isExtrFilter_iff` `eq_of_nhdsWithin`
`isLocalExtr_iff` 📖	mathematical	`Filter.EventuallyEq` `nhds`	`IsLocalExtr`	—	`isExtrFilter_iff` `eq_of_nhds`
`isLocalMaxOn_iff` 📖	mathematical	`Filter.EventuallyEq` `nhdsWithin` `Set` `Set.instMembership`	`IsLocalMaxOn`	—	`isMaxFilter_iff` `eq_of_nhdsWithin`
`isLocalMax_iff` 📖	mathematical	`Filter.EventuallyEq` `nhds`	`IsLocalMax`	—	`isMaxFilter_iff` `eq_of_nhds`
`isLocalMinOn_iff` 📖	mathematical	`Filter.EventuallyEq` `nhdsWithin` `Set` `Set.instMembership`	`IsLocalMinOn`	—	`isMinFilter_iff` `eq_of_nhdsWithin`
`isLocalMin_iff` 📖	mathematical	`Filter.EventuallyEq` `nhds`	`IsLocalMin`	—	`isMinFilter_iff` `eq_of_nhds`

Filter.EventuallyLE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLocalMax` 📖	mathematical	`Filter.EventuallyLE` `Preorder.toLE` `nhds` `IsLocalMax`	`IsLocalMax`	—	`isMaxFilter`
`isLocalMaxOn` 📖	mathematical	`Filter.EventuallyLE` `Preorder.toLE` `nhdsWithin` `IsLocalMaxOn`	`IsLocalMaxOn`	—	`isMaxFilter`
`isLocalMin` 📖	mathematical	`Filter.EventuallyLE` `Preorder.toLE` `nhds` `IsLocalMin`	`IsLocalMin`	—	`isMinFilter`
`isLocalMinOn` 📖	mathematical	`Filter.EventuallyLE` `Preorder.toLE` `nhdsWithin` `IsLocalMinOn`	`IsLocalMinOn`	—	`isMinFilter`

IsExtrOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLocalExtr` 📖	mathematical	`IsExtrOn` `Set` `Filter` `Filter.instMembership` `nhds`	`IsLocalExtr`	—	`IsLocalExtrOn.isLocalExtr` `localize`
`localize` 📖	mathematical	`IsExtrOn`	`IsLocalExtrOn`	—	`IsExtrFilter.filter_mono` `inf_le_right`

IsLocalExtr

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_antitone` 📖	mathematical	`IsLocalExtr` `Antitone`	`IsLocalExtr`	—	`IsExtrFilter.comp_antitone`
`comp_continuous` 📖	mathematical	`IsLocalExtr` `ContinuousAt`	`IsLocalExtr`	—	`IsExtrFilter.comp_tendsto`
`comp_continuousOn` 📖	mathematical	`IsLocalExtr` `ContinuousOn` `Set` `Set.instMembership`	`IsLocalExtrOn`	—	`elim` `IsMinFilter.isExtr` `IsLocalMin.comp_continuousOn` `IsMaxFilter.isExtr` `IsLocalMax.comp_continuousOn`
`comp_mono` 📖	mathematical	`IsLocalExtr` `Monotone`	`IsLocalExtr`	—	`IsExtrFilter.comp_mono`
`elim` 📖	—	`IsLocalExtr`	—	—	—
`neg` 📖	mathematical	`IsLocalExtr` `PartialOrder.toPreorder`	`IsLocalExtr` `PartialOrder.toPreorder` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`IsExtrFilter.neg`
`on` 📖	mathematical	`IsLocalExtr`	`IsLocalExtrOn`	—	`IsExtrFilter.filter_inf`

IsLocalExtrOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_antitone` 📖	mathematical	`IsLocalExtrOn` `Antitone`	`IsLocalExtrOn`	—	`IsExtrFilter.comp_antitone`
`comp_continuousOn` 📖	mathematical	`IsLocalExtrOn` `Set` `Set.instHasSubset` `Set.preimage` `ContinuousOn` `Set.instMembership`	`IsLocalExtrOn`	—	`elim` `IsMinFilter.isExtr` `IsLocalMinOn.comp_continuousOn` `IsMaxFilter.isExtr` `IsLocalMaxOn.comp_continuousOn`
`comp_mono` 📖	mathematical	`IsLocalExtrOn` `Monotone`	`IsLocalExtrOn`	—	`IsExtrFilter.comp_mono`
`elim` 📖	—	`IsLocalExtrOn`	—	—	—
`inter` 📖	mathematical	`IsLocalExtrOn`	`IsLocalExtrOn` `Set` `Set.instInter`	—	`on_subset` `Set.inter_subset_left`
`isLocalExtr` 📖	mathematical	`IsLocalExtrOn` `Set` `Filter` `Filter.instMembership` `nhds`	`IsLocalExtr`	—	`elim` `IsMinFilter.isExtr` `IsLocalMinOn.isLocalMin` `IsMaxFilter.isExtr` `IsLocalMaxOn.isLocalMax`
`neg` 📖	mathematical	`IsLocalExtrOn` `PartialOrder.toPreorder`	`IsLocalExtrOn` `PartialOrder.toPreorder` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`IsExtrFilter.neg`
`not_nhds_le_map` 📖	mathematical	`IsLocalExtrOn`	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhds` `Filter.map` `nhdsWithin`	—	`elim` `IsLocalMinOn.not_nhds_le_map` `IsLocalMaxOn.not_nhds_le_map`
`on_subset` 📖	mathematical	`IsLocalExtrOn` `Set` `Set.instHasSubset`	`IsLocalExtrOn`	—	`IsExtrFilter.filter_mono` `nhdsWithin_mono`

IsLocalMax

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`IsLocalMax` `PartialOrder.toPreorder`	`IsLocalMax` `PartialOrder.toPreorder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`IsMaxFilter.add`
`bicomp_mono` 📖	mathematical	`Relator.LiftFun` `Preorder.toLE` `IsLocalMax`	`IsLocalMax`	—	`IsMaxFilter.bicomp_mono`
`comp_antitone` 📖	mathematical	`IsLocalMax` `Antitone`	`IsLocalMin`	—	`IsMaxFilter.comp_antitone`
`comp_continuous` 📖	mathematical	`IsLocalMax` `ContinuousAt`	`IsLocalMax`	—	—
`comp_continuousOn` 📖	mathematical	`IsLocalMax` `ContinuousOn` `Set` `Set.instMembership`	`IsLocalMaxOn`	—	`IsMaxFilter.comp_tendsto`
`comp_mono` 📖	mathematical	`IsLocalMax` `Monotone`	`IsLocalMax`	—	`IsMaxFilter.comp_mono`
`inf` 📖	mathematical	`IsLocalMax` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder`	`IsLocalMax` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `SemilatticeInf.toMin`	—	`IsMaxFilter.inf`
`max` 📖	mathematical	`IsLocalMax` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`IsLocalMax` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`IsMaxFilter.max`
`min` 📖	mathematical	`IsLocalMax` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`IsLocalMax` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeInf.toMin`	—	`IsMaxFilter.min`
`neg` 📖	mathematical	`IsLocalMax` `PartialOrder.toPreorder`	`IsLocalMin` `PartialOrder.toPreorder` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`IsMaxFilter.neg`
`on` 📖	mathematical	`IsLocalMax`	`IsLocalMaxOn`	—	`IsMaxFilter.filter_inf`
`sub` 📖	mathematical	`IsLocalMax` `PartialOrder.toPreorder` `IsLocalMin`	`IsLocalMax` `PartialOrder.toPreorder` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`IsMaxFilter.sub`
`sup` 📖	mathematical	`IsLocalMax` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	`IsLocalMax` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SemilatticeSup.toMax`	—	`IsMaxFilter.sup`

IsLocalMaxOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`IsLocalMaxOn` `PartialOrder.toPreorder`	`IsLocalMaxOn` `PartialOrder.toPreorder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`IsMaxFilter.add`
`bicomp_mono` 📖	mathematical	`Relator.LiftFun` `Preorder.toLE` `IsLocalMaxOn`	`IsLocalMaxOn`	—	`IsMaxFilter.bicomp_mono`
`comp_antitone` 📖	mathematical	`IsLocalMaxOn` `Antitone`	`IsLocalMinOn`	—	`IsMaxFilter.comp_antitone`
`comp_continuousOn` 📖	mathematical	`IsLocalMaxOn` `Set` `Set.instHasSubset` `Set.preimage` `ContinuousOn` `Set.instMembership`	`IsLocalMaxOn`	—	`IsMaxFilter.comp_tendsto` `tendsto_nhdsWithin_mono_right` `Set.image_subset_iff` `ContinuousWithinAt.tendsto_nhdsWithin_image`
`comp_mono` 📖	mathematical	`IsLocalMaxOn` `Monotone`	`IsLocalMaxOn`	—	`IsMaxFilter.comp_mono`
`inf` 📖	mathematical	`IsLocalMaxOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder`	`IsLocalMaxOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `SemilatticeInf.toMin`	—	`IsMaxFilter.inf`
`inter` 📖	mathematical	`IsLocalMaxOn`	`IsLocalMaxOn` `Set` `Set.instInter`	—	`on_subset` `Set.inter_subset_left`
`isLocalMax` 📖	mathematical	`IsLocalMaxOn` `Set` `Filter` `Filter.instMembership` `nhds`	`IsLocalMax`	—	`Filter.le_principal_iff` `IsMaxFilter.filter_mono` `le_inf` `le_rfl`
`max` 📖	mathematical	`IsLocalMaxOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`IsLocalMaxOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`IsMaxFilter.max`
`min` 📖	mathematical	`IsLocalMaxOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`IsLocalMaxOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeInf.toMin`	—	`IsMaxFilter.min`
`neg` 📖	mathematical	`IsLocalMaxOn` `PartialOrder.toPreorder`	`IsLocalMinOn` `PartialOrder.toPreorder` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`IsMaxFilter.neg`
`not_nhds_le_map` 📖	mathematical	`IsLocalMaxOn`	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhds` `Filter.map` `nhdsWithin`	—	`IsLocalMinOn.not_nhds_le_map`
`on_subset` 📖	mathematical	`IsLocalMaxOn` `Set` `Set.instHasSubset`	`IsLocalMaxOn`	—	`IsMaxFilter.filter_mono` `nhdsWithin_mono`
`sub` 📖	mathematical	`IsLocalMaxOn` `PartialOrder.toPreorder` `IsLocalMinOn`	`IsLocalMaxOn` `PartialOrder.toPreorder` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`IsMaxFilter.sub`
`sup` 📖	mathematical	`IsLocalMaxOn` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	`IsLocalMaxOn` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SemilatticeSup.toMax`	—	`IsMaxFilter.sup`

IsLocalMin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`IsLocalMin` `PartialOrder.toPreorder`	`IsLocalMin` `PartialOrder.toPreorder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`IsMinFilter.add`
`bicomp_mono` 📖	mathematical	`Relator.LiftFun` `Preorder.toLE` `IsLocalMin`	`IsLocalMin`	—	`IsMinFilter.bicomp_mono`
`comp_antitone` 📖	mathematical	`IsLocalMin` `Antitone`	`IsLocalMax`	—	`IsMinFilter.comp_antitone`
`comp_continuous` 📖	mathematical	`IsLocalMin` `ContinuousAt`	`IsLocalMin`	—	—
`comp_continuousOn` 📖	mathematical	`IsLocalMin` `ContinuousOn` `Set` `Set.instMembership`	`IsLocalMinOn`	—	`IsMinFilter.comp_tendsto`
`comp_mono` 📖	mathematical	`IsLocalMin` `Monotone`	`IsLocalMin`	—	`IsMinFilter.comp_mono`
`inf` 📖	mathematical	`IsLocalMin` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder`	`IsLocalMin` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `SemilatticeInf.toMin`	—	`IsMinFilter.inf`
`max` 📖	mathematical	`IsLocalMin` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`IsLocalMin` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`IsMinFilter.max`
`min` 📖	mathematical	`IsLocalMin` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`IsLocalMin` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeInf.toMin`	—	`IsMinFilter.min`
`neg` 📖	mathematical	`IsLocalMin` `PartialOrder.toPreorder`	`IsLocalMax` `PartialOrder.toPreorder` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`IsMinFilter.neg`
`on` 📖	mathematical	`IsLocalMin`	`IsLocalMinOn`	—	`IsMinFilter.filter_inf`
`sub` 📖	mathematical	`IsLocalMin` `PartialOrder.toPreorder` `IsLocalMax`	`IsLocalMin` `PartialOrder.toPreorder` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`IsMinFilter.sub`
`sup` 📖	mathematical	`IsLocalMin` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	`IsLocalMin` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SemilatticeSup.toMax`	—	`IsMinFilter.sup`

IsLocalMinOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`IsLocalMinOn` `PartialOrder.toPreorder`	`IsLocalMinOn` `PartialOrder.toPreorder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`IsMinFilter.add`
`bicomp_mono` 📖	mathematical	`Relator.LiftFun` `Preorder.toLE` `IsLocalMinOn`	`IsLocalMinOn`	—	`IsMinFilter.bicomp_mono`
`comp_antitone` 📖	mathematical	`IsLocalMinOn` `Antitone`	`IsLocalMaxOn`	—	`IsMinFilter.comp_antitone`
`comp_continuousOn` 📖	mathematical	`IsLocalMinOn` `Set` `Set.instHasSubset` `Set.preimage` `ContinuousOn` `Set.instMembership`	`IsLocalMinOn`	—	`IsMinFilter.comp_tendsto` `tendsto_nhdsWithin_mono_right` `Set.image_subset_iff` `ContinuousWithinAt.tendsto_nhdsWithin_image`
`comp_mono` 📖	mathematical	`IsLocalMinOn` `Monotone`	`IsLocalMinOn`	—	`IsMinFilter.comp_mono`
`inf` 📖	mathematical	`IsLocalMinOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder`	`IsLocalMinOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `SemilatticeInf.toMin`	—	`IsMinFilter.inf`
`inter` 📖	mathematical	`IsLocalMinOn`	`IsLocalMinOn` `Set` `Set.instInter`	—	`on_subset` `Set.inter_subset_left`
`isLocalMin` 📖	mathematical	`IsLocalMinOn` `Set` `Filter` `Filter.instMembership` `nhds`	`IsLocalMin`	—	`Filter.le_principal_iff` `IsMinFilter.filter_mono` `le_inf` `le_rfl`
`max` 📖	mathematical	`IsLocalMinOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`IsLocalMinOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`IsMinFilter.max`
`min` 📖	mathematical	`IsLocalMinOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`IsLocalMinOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeInf.toMin`	—	`IsMinFilter.min`
`neg` 📖	mathematical	`IsLocalMinOn` `PartialOrder.toPreorder`	`IsLocalMaxOn` `PartialOrder.toPreorder` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`IsMinFilter.neg`
`not_nhds_le_map` 📖	mathematical	`IsLocalMinOn`	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhds` `Filter.map` `nhdsWithin`	—	`Filter.Eventually.filter_mono` `LE.le.trans` `inf_le_left` `Filter.eventually_map` `Filter.Eventually.exists` `Filter.Eventually.and` `self_mem_nhdsWithin` `LE.le.not_gt`
`on_subset` 📖	mathematical	`IsLocalMinOn` `Set` `Set.instHasSubset`	`IsLocalMinOn`	—	`IsMinFilter.filter_mono` `nhdsWithin_mono`
`sub` 📖	mathematical	`IsLocalMinOn` `PartialOrder.toPreorder` `IsLocalMaxOn`	`IsLocalMinOn` `PartialOrder.toPreorder` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`IsMinFilter.sub`
`sup` 📖	mathematical	`IsLocalMinOn` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	`IsLocalMinOn` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SemilatticeSup.toMax`	—	`IsMinFilter.sup`

IsMaxOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLocalMax` 📖	mathematical	`IsMaxOn` `Set` `Filter` `Filter.instMembership` `nhds`	`IsLocalMax`	—	`IsLocalMaxOn.isLocalMax` `localize`
`localize` 📖	mathematical	`IsMaxOn`	`IsLocalMaxOn`	—	`IsMaxFilter.filter_mono` `inf_le_right`

IsMinOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLocalMin` 📖	mathematical	`IsMinOn` `Set` `Filter` `Filter.instMembership` `nhds`	`IsLocalMin`	—	`IsLocalMinOn.isLocalMin` `localize`
`localize` 📖	mathematical	`IsMinOn`	`IsLocalMinOn`	—	`IsMinFilter.filter_mono` `inf_le_right`

(root)

Definitions

Name	Category	Theorems
`IsLocalExtr` 📖	MathDef	16 math math: `IsLocalExtr.comp_antitone`, `IsLocalExtr.neg`, `exists_isLocalExtr_Ioo`, `IsLocalExtr.comp_mono`, `exists_isLocalExtr_Ioo_of_tendsto`, `IsExtrOn.isLocalExtr`, `isLocalExtr_const`, `exists_isLocalExtr_uIoo_of_tendsto`, `exists_isLocalExtr_uIoo`, `Polynomial.Chebyshev.isLocalExtr_T_real_iff`, `Filter.EventuallyEq.isLocalExtr_iff`, `IsLocalExtr.comp_continuous`, `Polynomial.Chebyshev.isLocalExtr_T_real`, `IsLocalExtr.congr`, `IsLocalExtrOn.isLocalExtr`, `isLocalExtrOn_univ_iff`
`IsLocalExtrOn` 📖	MathDef	14 math math: `IsExtrOn.localize`, `IsLocalExtrOn.neg`, `IsLocalExtrOn.comp_antitone`, `isLocalExtrOn_const`, `IsLocalExtrOn.comp_continuousOn`, `IsLocalExtrOn.comp_mono`, `IsLocalExtrOn.on_subset`, `IsLocalExtrOn.closure`, `IsLocalExtr.on`, `IsLocalExtrOn.congr`, `IsLocalExtrOn.inter`, `IsLocalExtr.comp_continuousOn`, `Filter.EventuallyEq.isLocalExtrOn_iff`, `isLocalExtrOn_univ_iff`
`IsLocalMax` 📖	MathDef	30 math math: `isLocalMax_of_deriv'`, `Filter.EventuallyLE.isLocalMax`, `isLocalMax_of_sign_deriv`, `Filter.EventuallyEq.isLocalMax_iff`, `IsLocalMax.congr`, `Polynomial.Chebyshev.isLocalMax_T_real`, `IsMaxOn.isLocalMax`, `IsLocalMax.norm_add_sameRay`, `IsLocalMin.neg`, `IsLocalMax.sub`, `IsLocalMax.bicomp_mono`, `IsCompact.exists_isLocalMax_mem_open`, `IsLocalMax.min`, `isLocalMax_of_deriv_deriv_neg`, `IsLocalMax.sup`, `IsLocalMax.max`, `IsLocalMin.comp_antitone`, `isLocalMax_of_mono_anti'`, `IsLocalMin.inv`, `IsLocalMaxOn.isLocalMax`, `IsLocalMax.comp_mono`, `IsLocalMax.add`, `isLocalMax_const`, `isLocalMax_of_deriv`, `IsLocalMax.norm_add_self`, `isLocalMax_of_mono_anti`, `IsLocalMax.inf`, `isLocalMaxOn_univ_iff`, `isLocalMax_of_deriv_Ioo`, `IsLocalMax.comp_continuous`
`IsLocalMaxOn` 📖	MathDef	24 math math: `IsLocalMaxOn.max`, `IsLocalMaxOn.norm_add_self`, `IsLocalMinOn.comp_antitone`, `isLocalMaxOn_const`, `IsLocalMinOn.neg`, `IsLocalMaxOn.norm_add_sameRay`, `IsLocalMaxOn.inter`, `IsLocalMax.comp_continuousOn`, `IsMaxOn.localize`, `IsLocalMaxOn.congr`, `IsLocalMaxOn.inf`, `IsLocalMaxOn.bicomp_mono`, `IsLocalMaxOn.on_subset`, `IsLocalMaxOn.sup`, `IsLocalMaxOn.min`, `IsLocalMaxOn.comp_continuousOn`, `IsLocalMaxOn.sub`, `Filter.EventuallyLE.isLocalMaxOn`, `IsLocalMaxOn.comp_mono`, `isLocalMaxOn_univ_iff`, `IsLocalMaxOn.add`, `IsLocalMaxOn.closure`, `IsLocalMax.on`, `Filter.EventuallyEq.isLocalMaxOn_iff`
`IsLocalMin` 📖	MathDef	28 math math: `isLocalMinOn_univ_iff`, `IsLocalMin.sub`, `IsLocalMin.add`, `Filter.EventuallyLE.isLocalMin`, `Metric.exists_isLocalMin_mem_ball`, `Polynomial.Chebyshev.isLocalMin_T_real`, `isLocalMin_of_deriv_deriv_pos`, `IsLocalMin.sup`, `IsLocalMin.comp_mono`, `IsLocalMinOn.isLocalMin`, `isLocalMin_of_anti_mono'`, `IsLocalMin.inf`, `isLocalMin_of_deriv'`, `IsLocalMin.max`, `IsMinOn.isLocalMin`, `isLocalMin_of_anti_mono`, `IsLocalMin.comp_continuous`, `isLocalMin_const`, `IsCompact.exists_isLocalMin_mem_open`, `Filter.EventuallyEq.isLocalMin_iff`, `IsLocalMax.neg`, `isLocalMin_of_sign_deriv`, `IsLocalMax.comp_antitone`, `IsLocalMin.bicomp_mono`, `IsLocalMin.congr`, `isLocalMin_of_deriv_Ioo`, `isLocalMin_of_deriv`, `IsLocalMin.min`
`IsLocalMinOn` 📖	MathDef	22 math math: `isLocalMinOn_univ_iff`, `IsLocalMinOn.sub`, `IsLocalMinOn.inf`, `IsLocalMinOn.min`, `IsLocalMinOn.max`, `Filter.EventuallyEq.isLocalMinOn_iff`, `IsLocalMinOn.bicomp_mono`, `IsLocalMaxOn.neg`, `IsLocalMinOn.comp_mono`, `IsLocalMaxOn.comp_antitone`, `IsLocalMinOn.comp_continuousOn`, `IsLocalMinOn.closure`, `isLocalMinOn_const`, `IsLocalMin.comp_continuousOn`, `IsLocalMin.on`, `IsLocalMinOn.add`, `IsLocalMinOn.inter`, `Filter.EventuallyLE.isLocalMinOn`, `IsMinOn.localize`, `IsLocalMinOn.sup`, `IsLocalMinOn.on_subset`, `IsLocalMinOn.congr`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLocalExtrOn_const` 📖	mathematical	—	`IsLocalExtrOn`	—	`isExtrFilter_const`
`isLocalExtrOn_univ_iff` 📖	mathematical	—	`IsLocalExtrOn` `Set.univ` `IsLocalExtr`	—	`Iff.or` `isLocalMinOn_univ_iff` `isLocalMaxOn_univ_iff`
`isLocalExtr_const` 📖	mathematical	—	`IsLocalExtr`	—	`isExtrFilter_const`
`isLocalMaxOn_const` 📖	mathematical	—	`IsLocalMaxOn`	—	`isMaxFilter_const`
`isLocalMaxOn_univ_iff` 📖	mathematical	—	`IsLocalMaxOn` `Set.univ` `IsLocalMax`	—	`nhdsWithin_univ`
`isLocalMax_const` 📖	mathematical	—	`IsLocalMax`	—	`isMaxFilter_const`
`isLocalMax_of_mono_anti'` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhdsWithin` `Set.Iic` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ici` `MonotoneOn` `AntitoneOn`	`IsLocalMax`	—	`mem_of_mem_nhdsWithin` `instReflLe` `Filter.mem_of_superset` `nhds_of_Ici_Iic` `le_total`
`isLocalMinOn_const` 📖	mathematical	—	`IsLocalMinOn`	—	`isMinFilter_const`
`isLocalMinOn_univ_iff` 📖	mathematical	—	`IsLocalMinOn` `Set.univ` `IsLocalMin`	—	`nhdsWithin_univ`
`isLocalMin_const` 📖	mathematical	—	`IsLocalMin`	—	`isMinFilter_const`
`isLocalMin_of_anti_mono'` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhdsWithin` `Set.Iic` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ici` `AntitoneOn` `MonotoneOn`	`IsLocalMin`	—	`mem_of_mem_nhdsWithin` `instReflLe` `Filter.mem_of_superset` `nhds_of_Ici_Iic` `le_total`

---

← Back to Index