Extr

📁 Source: Mathlib/Order/Filter/Extr.lean

Statistics

Metric	Count
Definitions `IsExtrFilter`, `IsExtrOn`, `IsMaxFilter`, `IsMaxOn`, `IsMinFilter`, `IsMinOn`	6
Theorems `isExtrFilter_iff`, `isMaxFilter_iff`, `isMinFilter_iff`, `isMaxFilter`, `isMinFilter`, `comp_antitone`, `comp_mono`, `comp_tendsto`, `dual`, `filter_inf`, `filter_mono`, `neg`, `undual`, `comp_antitone`, `comp_mapsTo`, `comp_mono`, `dual`, `elim`, `inter`, `neg`, `on_preimage`, `on_subset`, `undual`, `add`, `bicomp_mono`, `comp_antitone`, `comp_mono`, `comp_tendsto`, `dual`, `filter_inf`, `filter_mono`, `inf`, `isExtr`, `max`, `min`, `neg`, `sub`, `sup`, `tendsto_principal_Iic`, `undual`, `add`, `bddAbove`, `bicomp_mono`, `comp_antitone`, `comp_mapsTo`, `comp_mono`, `dual`, `iSup_eq`, `inf`, `inter`, `isExtr`, `isLUB`, `max`, `min`, `neg`, `on_preimage`, `on_subset`, `sub`, `sup`, `undual`, `add`, `bicomp_mono`, `comp_antitone`, `comp_mono`, `comp_tendsto`, `dual`, `filter_inf`, `filter_mono`, `inf`, `isExtr`, `max`, `min`, `neg`, `sub`, `sup`, `tendsto_principal_Ici`, `undual`, `add`, `bddBelow`, `bicomp_mono`, `comp_antitone`, `comp_mapsTo`, `comp_mono`, `dual`, `iInf_eq`, `inf`, `inter`, `isExtr`, `isGLB`, `max`, `min`, `neg`, `on_preimage`, `on_subset`, `sub`, `sup`, `undual`, `eventuallyEq_of_isMinFilter_of_isMaxFilter`, `inf_eq_of_isMinOn`, `inf_eq_of_min`, `isExtrFilter_const`, `isExtrFilter_dual_iff`, `isExtrOn_const`, `isExtrOn_dual_iff`, `isMaxFilter_const`, `isMaxFilter_dual_iff`, `isMaxOn_const`, `isMaxOn_dual_iff`, `isMaxOn_iff`, `isMaxOn_univ_iff`, `isMinFilter_const`, `isMinFilter_dual_iff`, `isMinOn_const`, `isMinOn_dual_iff`, `isMinOn_iff`, `isMinOn_univ_iff`, `sup_eq_of_isMaxOn`, `sup_eq_of_max`	118
Total	124

Filter.EventuallyEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isExtrFilter_iff` 📖	mathematical	`Filter.EventuallyEq`	`IsExtrFilter`	—	`IsExtrFilter.congr` `symm`
`isMaxFilter_iff` 📖	mathematical	`Filter.EventuallyEq`	`IsMaxFilter`	—	`IsMaxFilter.congr` `symm`
`isMinFilter_iff` 📖	mathematical	`Filter.EventuallyEq`	`IsMinFilter`	—	`IsMinFilter.congr` `symm`

Filter.EventuallyLE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isMaxFilter` 📖	mathematical	`Filter.EventuallyLE` `Preorder.toLE` `IsMaxFilter`	`IsMaxFilter`	—	`Filter.Eventually.mp` `Filter.Eventually.mono` `le_trans`
`isMinFilter` 📖	mathematical	`Filter.EventuallyLE` `Preorder.toLE` `IsMinFilter`	`IsMinFilter`	—	`isMaxFilter`

IsExtrFilter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_antitone` 📖	mathematical	`IsExtrFilter` `Antitone`	`IsExtrFilter`	—	`comp_mono` `dual`
`comp_mono` 📖	mathematical	`IsExtrFilter` `Monotone`	`IsExtrFilter`	—	`IsMinFilter.isExtr` `IsMinFilter.comp_mono` `IsMaxFilter.isExtr` `IsMaxFilter.comp_mono`
`comp_tendsto` 📖	mathematical	`IsExtrFilter` `Filter.Tendsto`	`IsExtrFilter`	—	`IsMinFilter.isExtr` `IsMinFilter.comp_tendsto` `IsMaxFilter.isExtr` `IsMaxFilter.comp_tendsto`
`dual` 📖	mathematical	`IsExtrFilter`	`IsExtrFilter` `OrderDual` `OrderDual.instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	`isExtrFilter_dual_iff`
`filter_inf` 📖	mathematical	`IsExtrFilter`	`IsExtrFilter` `Filter` `Filter.instInf`	—	`filter_mono` `inf_le_left`
`filter_mono` 📖	mathematical	`IsExtrFilter` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder`	`IsExtrFilter`	—	`IsMinFilter.isExtr` `IsMinFilter.filter_mono` `IsMaxFilter.isExtr` `IsMaxFilter.filter_mono`
`neg` 📖	mathematical	`IsExtrFilter` `PartialOrder.toPreorder`	`IsExtrFilter` `PartialOrder.toPreorder` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`IsMaxFilter.isExtr` `IsMinFilter.neg` `IsMinFilter.isExtr` `IsMaxFilter.neg`
`undual` 📖	mathematical	`IsExtrFilter` `OrderDual` `OrderDual.instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	`IsExtrFilter`	—	`isExtrFilter_dual_iff`

IsExtrOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_antitone` 📖	mathematical	`IsExtrOn` `Antitone`	`IsExtrOn`	—	`IsExtrFilter.comp_antitone`
`comp_mapsTo` 📖	mathematical	`IsExtrOn` `Set.MapsTo`	`IsExtrOn`	—	`elim` `IsMinOn.comp_mapsTo` `IsMaxOn.comp_mapsTo`
`comp_mono` 📖	mathematical	`IsExtrOn` `Monotone`	`IsExtrOn`	—	`IsExtrFilter.comp_mono`
`dual` 📖	mathematical	`IsExtrOn`	`IsExtrOn` `OrderDual` `OrderDual.instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	`isExtrOn_dual_iff`
`elim` 📖	—	`IsExtrOn`	—	—	—
`inter` 📖	mathematical	`IsExtrOn`	`IsExtrOn` `Set` `Set.instInter`	—	`on_subset` `Set.inter_subset_left`
`neg` 📖	mathematical	`IsExtrOn` `PartialOrder.toPreorder`	`IsExtrOn` `PartialOrder.toPreorder` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`elim` `IsMaxOn.isExtr` `IsMinOn.neg` `IsMinOn.isExtr` `IsMaxOn.neg`
`on_preimage` 📖	mathematical	`IsExtrOn`	`IsExtrOn` `Set.preimage`	—	`elim` `IsMinOn.isExtr` `IsMinOn.on_preimage` `IsMaxOn.isExtr` `IsMaxOn.on_preimage`
`on_subset` 📖	mathematical	`IsExtrOn` `Set` `Set.instHasSubset`	`IsExtrOn`	—	`IsExtrFilter.filter_mono` `Filter.principal_mono`
`undual` 📖	mathematical	`IsExtrOn` `OrderDual` `OrderDual.instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	`IsExtrOn`	—	`isExtrOn_dual_iff`

IsMaxFilter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`IsMaxFilter` `PartialOrder.toPreorder`	`IsMaxFilter` `PartialOrder.toPreorder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`bicomp_mono` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add`
`bicomp_mono` 📖	mathematical	`Relator.LiftFun` `Preorder.toLE` `IsMaxFilter`	`IsMaxFilter`	—	`Filter.mem_of_superset` `Filter.inter_mem`
`comp_antitone` 📖	mathematical	`IsMaxFilter` `Antitone`	`IsMinFilter`	—	`IsMinFilter.comp_mono` `dual`
`comp_mono` 📖	mathematical	`IsMaxFilter` `Monotone`	`IsMaxFilter`	—	`Filter.mem_of_superset`
`comp_tendsto` 📖	mathematical	`IsMaxFilter` `Filter.Tendsto`	`IsMaxFilter`	—	—
`dual` 📖	mathematical	`IsMaxFilter`	`IsMinFilter` `OrderDual` `OrderDual.instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	`isMinFilter_dual_iff`
`filter_inf` 📖	mathematical	`IsMaxFilter`	`IsMaxFilter` `Filter` `Filter.instInf`	—	`filter_mono` `inf_le_left`
`filter_mono` 📖	mathematical	`IsMaxFilter` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder`	`IsMaxFilter`	—	—
`inf` 📖	mathematical	`IsMaxFilter` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder`	`IsMaxFilter` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `SemilatticeInf.toMin`	—	`bicomp_mono` `inf_le_inf`
`isExtr` 📖	mathematical	`IsMaxFilter`	`IsExtrFilter`	—	—
`max` 📖	mathematical	`IsMaxFilter` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`IsMaxFilter` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`bicomp_mono` `max_le_max`
`min` 📖	mathematical	`IsMaxFilter` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`IsMaxFilter` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeInf.toMin`	—	`bicomp_mono` `min_le_min`
`neg` 📖	mathematical	`IsMaxFilter` `PartialOrder.toPreorder`	`IsMinFilter` `PartialOrder.toPreorder` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`comp_antitone` `neg_le_neg`
`sub` 📖	mathematical	`IsMaxFilter` `PartialOrder.toPreorder` `IsMinFilter`	`IsMaxFilter` `PartialOrder.toPreorder` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`sub_eq_add_neg` `add` `IsMinFilter.neg`
`sup` 📖	mathematical	`IsMaxFilter` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	`IsMaxFilter` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SemilatticeSup.toMax`	—	`bicomp_mono` `sup_le_sup`
`tendsto_principal_Iic` 📖	mathematical	`IsMaxFilter`	`Filter.Tendsto` `Filter.principal` `Set.Iic`	—	`Filter.tendsto_principal`
`undual` 📖	mathematical	`IsMaxFilter` `OrderDual` `OrderDual.instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	`IsMinFilter`	—	`isMaxFilter_dual_iff`

IsMaxOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`IsMaxOn` `PartialOrder.toPreorder`	`IsMaxOn` `PartialOrder.toPreorder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`IsMaxFilter.add`
`bddAbove` 📖	mathematical	`IsMaxOn`	`BddAbove` `Preorder.toLE` `Set.image`	—	—
`bicomp_mono` 📖	mathematical	`Relator.LiftFun` `Preorder.toLE` `IsMaxOn`	`IsMaxOn`	—	`IsMaxFilter.bicomp_mono`
`comp_antitone` 📖	mathematical	`IsMaxOn` `Antitone`	`IsMinOn`	—	`IsMaxFilter.comp_antitone`
`comp_mapsTo` 📖	mathematical	`IsMaxOn` `Set.MapsTo`	`IsMaxOn`	—	`IsMinOn.comp_mapsTo` `dual`
`comp_mono` 📖	mathematical	`IsMaxOn` `Monotone`	`IsMaxOn`	—	`IsMaxFilter.comp_mono`
`dual` 📖	mathematical	`IsMaxOn`	`IsMinOn` `OrderDual` `OrderDual.instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	`isMinOn_dual_iff`
`iSup_eq` 📖	mathematical	`Set` `Set.instMembership` `IsMaxOn` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`iSup` `Set.Elem` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Set` `Set.instMembership`	—	`ciSup_eq_of_forall_le_of_forall_lt_exists_gt`
`inf` 📖	mathematical	`IsMaxOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder`	`IsMaxOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `SemilatticeInf.toMin`	—	`IsMaxFilter.inf`
`inter` 📖	mathematical	`IsMaxOn`	`IsMaxOn` `Set` `Set.instInter`	—	`on_subset` `Set.inter_subset_left`
`isExtr` 📖	mathematical	`IsMaxOn`	`IsExtrOn`	—	`IsMaxFilter.isExtr`
`isLUB` 📖	mathematical	`Set` `Set.instMembership` `IsMaxOn`	`IsLUB` `Preorder.toLE` `setOf` `Set` `Set.instMembership`	—	`IsMinOn.isGLB`
`max` 📖	mathematical	`IsMaxOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`IsMaxOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`IsMaxFilter.max`
`min` 📖	mathematical	`IsMaxOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`IsMaxOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeInf.toMin`	—	`IsMaxFilter.min`
`neg` 📖	mathematical	`IsMaxOn` `PartialOrder.toPreorder`	`IsMinOn` `PartialOrder.toPreorder` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`comp_antitone` `neg_le_neg`
`on_preimage` 📖	mathematical	`IsMaxOn`	`IsMaxOn` `Set.preimage`	—	`IsMaxFilter.comp_tendsto` `Filter.tendsto_principal_principal` `Set.Subset.refl`
`on_subset` 📖	mathematical	`IsMaxOn` `Set` `Set.instHasSubset`	`IsMaxOn`	—	`IsMaxFilter.filter_mono` `Filter.principal_mono`
`sub` 📖	mathematical	`IsMaxOn` `PartialOrder.toPreorder` `IsMinOn`	`IsMaxOn` `PartialOrder.toPreorder` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`sub_eq_add_neg` `add` `IsMinOn.neg`
`sup` 📖	mathematical	`IsMaxOn` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	`IsMaxOn` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SemilatticeSup.toMax`	—	`IsMaxFilter.sup`
`undual` 📖	mathematical	`IsMaxOn` `OrderDual` `OrderDual.instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	`IsMinOn`	—	`isMaxOn_dual_iff`

IsMinFilter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`IsMinFilter` `PartialOrder.toPreorder`	`IsMinFilter` `PartialOrder.toPreorder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`bicomp_mono` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add`
`bicomp_mono` 📖	mathematical	`Relator.LiftFun` `Preorder.toLE` `IsMinFilter`	`IsMinFilter`	—	`Filter.mem_of_superset` `Filter.inter_mem`
`comp_antitone` 📖	mathematical	`IsMinFilter` `Antitone`	`IsMaxFilter`	—	`IsMaxFilter.comp_mono` `dual`
`comp_mono` 📖	mathematical	`IsMinFilter` `Monotone`	`IsMinFilter`	—	`Filter.mem_of_superset`
`comp_tendsto` 📖	mathematical	`IsMinFilter` `Filter.Tendsto`	`IsMinFilter`	—	—
`dual` 📖	mathematical	`IsMinFilter`	`IsMaxFilter` `OrderDual` `OrderDual.instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	`isMaxFilter_dual_iff`
`filter_inf` 📖	mathematical	`IsMinFilter`	`IsMinFilter` `Filter` `Filter.instInf`	—	`filter_mono` `inf_le_left`
`filter_mono` 📖	mathematical	`IsMinFilter` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder`	`IsMinFilter`	—	—
`inf` 📖	mathematical	`IsMinFilter` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder`	`IsMinFilter` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `SemilatticeInf.toMin`	—	`bicomp_mono` `inf_le_inf`
`isExtr` 📖	mathematical	`IsMinFilter`	`IsExtrFilter`	—	—
`max` 📖	mathematical	`IsMinFilter` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`IsMinFilter` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`bicomp_mono` `max_le_max`
`min` 📖	mathematical	`IsMinFilter` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`IsMinFilter` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeInf.toMin`	—	`bicomp_mono` `min_le_min`
`neg` 📖	mathematical	`IsMinFilter` `PartialOrder.toPreorder`	`IsMaxFilter` `PartialOrder.toPreorder` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`comp_antitone` `neg_le_neg`
`sub` 📖	mathematical	`IsMinFilter` `PartialOrder.toPreorder` `IsMaxFilter`	`IsMinFilter` `PartialOrder.toPreorder` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`sub_eq_add_neg` `add` `IsMaxFilter.neg`
`sup` 📖	mathematical	`IsMinFilter` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	`IsMinFilter` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SemilatticeSup.toMax`	—	`bicomp_mono` `sup_le_sup`
`tendsto_principal_Ici` 📖	mathematical	`IsMinFilter`	`Filter.Tendsto` `Filter.principal` `Set.Ici`	—	`Filter.tendsto_principal`
`undual` 📖	mathematical	`IsMinFilter` `OrderDual` `OrderDual.instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	`IsMaxFilter`	—	`isMinFilter_dual_iff`

IsMinOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`IsMinOn` `PartialOrder.toPreorder`	`IsMinOn` `PartialOrder.toPreorder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`IsMinFilter.add`
`bddBelow` 📖	mathematical	`IsMinOn`	`BddBelow` `Preorder.toLE` `Set.image`	—	—
`bicomp_mono` 📖	mathematical	`Relator.LiftFun` `Preorder.toLE` `IsMinOn`	`IsMinOn`	—	`IsMinFilter.bicomp_mono`
`comp_antitone` 📖	mathematical	`IsMinOn` `Antitone`	`IsMaxOn`	—	`IsMinFilter.comp_antitone`
`comp_mapsTo` 📖	mathematical	`IsMinOn` `Set.MapsTo`	`IsMinOn`	—	—
`comp_mono` 📖	mathematical	`IsMinOn` `Monotone`	`IsMinOn`	—	`IsMinFilter.comp_mono`
`dual` 📖	mathematical	`IsMinOn`	`IsMaxOn` `OrderDual` `OrderDual.instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	`isMaxOn_dual_iff`
`iInf_eq` 📖	mathematical	`Set` `Set.instMembership` `IsMinOn` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`iInf` `Set.Elem` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Set` `Set.instMembership`	—	`IsMaxOn.iSup_eq`
`inf` 📖	mathematical	`IsMinOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder`	`IsMinOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `SemilatticeInf.toMin`	—	`IsMinFilter.inf`
`inter` 📖	mathematical	`IsMinOn`	`IsMinOn` `Set` `Set.instInter`	—	`on_subset` `Set.inter_subset_left`
`isExtr` 📖	mathematical	`IsMinOn`	`IsExtrOn`	—	`IsMinFilter.isExtr`
`isGLB` 📖	mathematical	`Set` `Set.instMembership` `IsMinOn`	`IsGLB` `Preorder.toLE` `setOf` `Set` `Set.instMembership`	—	`isGLB_iff_le_iff` `le_trans`
`max` 📖	mathematical	`IsMinOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`IsMinOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`IsMinFilter.max`
`min` 📖	mathematical	`IsMinOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`IsMinOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeInf.toMin`	—	`IsMinFilter.min`
`neg` 📖	mathematical	`IsMinOn` `PartialOrder.toPreorder`	`IsMaxOn` `PartialOrder.toPreorder` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`comp_antitone` `neg_le_neg`
`on_preimage` 📖	mathematical	`IsMinOn`	`IsMinOn` `Set.preimage`	—	`IsMinFilter.comp_tendsto` `Filter.tendsto_principal_principal` `Set.Subset.refl`
`on_subset` 📖	mathematical	`IsMinOn` `Set` `Set.instHasSubset`	`IsMinOn`	—	`IsMinFilter.filter_mono` `Filter.principal_mono`
`sub` 📖	mathematical	`IsMinOn` `PartialOrder.toPreorder` `IsMaxOn`	`IsMinOn` `PartialOrder.toPreorder` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`sub_eq_add_neg` `add` `IsMaxOn.neg`
`sup` 📖	mathematical	`IsMinOn` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	`IsMinOn` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SemilatticeSup.toMax`	—	`IsMinFilter.sup`
`undual` 📖	mathematical	`IsMinOn` `OrderDual` `OrderDual.instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	`IsMaxOn`	—	`isMinOn_dual_iff`

(root)

Definitions

Name	Category	Theorems
`IsExtrFilter` 📖	MathDef	14 math math: `IsExtrFilter.congr`, `isExtrFilter_dual_iff`, `isExtrFilter_const`, `IsExtrFilter.comp_mono`, `IsExtrFilter.comp_tendsto`, `Filter.EventuallyEq.isExtrFilter_iff`, `IsMinFilter.isExtr`, `IsExtrFilter.dual`, `IsExtrFilter.filter_mono`, `IsMaxFilter.isExtr`, `IsExtrFilter.filter_inf`, `IsExtrFilter.neg`, `IsExtrFilter.undual`, `IsExtrFilter.comp_antitone`
`IsExtrOn` 📖	MathDef	20 math math: `Polynomial.Chebyshev.isExtrOn_T_real_iff`, `IsExtrOn.comp_antitone`, `IsExtrOn.closure`, `IsExtrOn.comp_mapsTo`, `IsMaxOn.isExtr`, `IsExtrOn.on_subset`, `exists_isExtrOn_Ioo_of_tendsto`, `IsExtrOn.undual`, `exists_isExtrOn_uIoo_of_tendsto`, `IsExtrOn.comp_mono`, `exists_Ioo_extr_on_Icc`, `IsMinOn.isExtr`, `isExtrOn_dual_iff`, `IsExtrOn.inter`, `IsExtrOn.on_preimage`, `IsExtrOn.dual`, `isExtrOn_const`, `Polynomial.Chebyshev.isExtrOn_T_real`, `IsExtrOn.neg`, `exists_uIoo_isExtrOn_uIcc`
`IsMaxFilter` 📖	MathDef	23 math math: `IsMaxFilter.filter_inf`, `IsMinFilter.dual`, `IsMaxFilter.congr`, `Filter.EventuallyLE.isMaxFilter`, `IsMaxFilter.add`, `IsMaxFilter.comp_mono`, `IsMaxFilter.inf`, `IsMaxFilter.filter_mono`, `Filter.EventuallyEq.isMaxFilter_iff`, `IsMaxFilter.max`, `IsMinFilter.neg`, `IsMaxFilter.bicomp_mono`, `IsMinFilter.undual`, `IsMaxFilter.min`, `isMaxFilter_const`, `IsMaxFilter.sub`, `IsMinFilter.comp_antitone`, `isMaxFilter_dual_iff`, `isMinFilter_dual_iff`, `IsMaxFilter.norm_add_self`, `IsMaxFilter.sup`, `IsMaxFilter.norm_add_sameRay`, `IsMaxFilter.comp_tendsto`
`IsMaxOn` 📖	MathDef	32 math math: `IsMinOn.comp_antitone`, `Complex.exists_mem_frontier_isMaxOn_norm`, `isMinOn_dual_iff`, `IsMaxOn.norm_add_self`, `IsMaxOn.sup`, `IsMaxOn.bicomp_mono`, `IsMaxOn.inf`, `IsMaxOn.on_preimage`, `IsMaxOn.comp_mapsTo`, `IsMaxOn.closure`, `isMaxOn_iff`, `IsMaxOn.of_isLocalMaxOn_of_concaveOn`, `Polynomial.Chebyshev.isMaxOn_T_real`, `isMaxOn_univ_iff`, `IsMaxOn.add`, `IsMaxOn.min`, `isMaxOn_const`, `IsMaxOn.on_subset`, `ContinuousOn.exists_isMaxOn'`, `IsMaxOn.comp_mono`, `Complex.isOpen_setOf_mem_nhds_and_isMaxOn_norm`, `UpperSemicontinuousOn.exists_isMaxOn`, `IsMaxOn.sub`, `isMaxOn_dual_iff`, `IsMinOn.neg`, `IsMinOn.undual`, `IsMaxOn.inter`, `IsCompact.exists_isMaxOn_mem_subset`, `IsCompact.exists_isMaxOn`, `IsMinOn.dual`, `IsMaxOn.max`, `IsMaxOn.norm_add_sameRay`
`IsMinFilter` 📖	MathDef	21 math math: `IsMinFilter.inf`, `IsMinFilter.sup`, `IsMinFilter.filter_mono`, `IsMinFilter.min`, `Filter.EventuallyLE.isMinFilter`, `IsMinFilter.comp_tendsto`, `IsMinFilter.add`, `IsMinFilter.congr`, `IsMinFilter.bicomp_mono`, `IsMaxFilter.neg`, `IsMaxFilter.comp_antitone`, `IsMaxFilter.undual`, `IsMinFilter.comp_mono`, `IsMinFilter.filter_inf`, `isMaxFilter_dual_iff`, `IsMinFilter.sub`, `isMinFilter_const`, `Filter.EventuallyEq.isMinFilter_iff`, `isMinFilter_dual_iff`, `IsMinFilter.max`, `IsMaxFilter.dual`
`IsMinOn` 📖	MathDef	35 math math: `IsMinOn.inter`, `isMinOn_dual_iff`, `IsMinOn.comp_mapsTo`, `IsMinOn.on_subset`, `IsMaxOn.undual`, `IsMinOn.min`, `IsMinOn.of_isLocalMinOn_of_convexOn_Icc`, `IsCompact.exists_isMinOn_mem_subset`, `Real.exists_isMinOn_Gamma_Ioi`, `NormedAlgebra.exists_isMinOn_norm_sub_smul`, `IsMaxOn.dual`, `IsMinOn.max`, `IsMaxOn.comp_antitone`, `IsMinOn.closure`, `IsMinOn.inf`, `Polynomial.Chebyshev.isMinOn_T_real`, `IsMinOn.of_isLocalMinOn_of_convexOn`, `IsMaxOn.neg`, `ConvexOn.isMinOn_of_leftDeriv_nonpos_of_rightDeriv_nonneg`, `IsCompact.exists_isMinOn`, `ContinuousOn.exists_isMinOn'`, `InformationTheory.isMinOn_klFun`, `IsMinOn.sup`, `IsMinOn.bicomp_mono`, `ConvexOn.isMinOn_of_rightDeriv_eq_zero`, `IsMinOn.sub`, `isMinOn_univ_iff`, `isMinOn_const`, `LowerSemicontinuousOn.exists_isMinOn`, `IsMinOn.comp_mono`, `isMaxOn_dual_iff`, `isMinOn_iff`, `ConvexOn.isMinOn_of_leftDeriv_eq_zero`, `IsMinOn.on_preimage`, `IsMinOn.add`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eventuallyEq_of_isMinFilter_of_isMaxFilter` 📖	mathematical	`IsMinFilter` `PartialOrder.toPreorder` `IsMaxFilter`	`Filter.EventuallyEq`	—	`Filter.mp_mem` `Filter.univ_mem'`
`inf_eq_of_isMinOn` 📖	mathematical	`Finset` `SetLike.instMembership` `Finset.instSetLike` `IsMinOn` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `SetLike.coe`	`Finset.inf`	—	`sup_eq_of_isMaxOn` `IsMinOn.dual`
`inf_eq_of_min` 📖	mathematical	`Set` `Set.instMembership` `Set.range` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Function.invFun` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder`	`Finset.inf`	—	`sup_eq_of_max` `OrderDual.instNonempty`
`isExtrFilter_const` 📖	mathematical	—	`IsExtrFilter`	—	`IsMinFilter.isExtr` `isMinFilter_const`
`isExtrFilter_dual_iff` 📖	mathematical	—	`IsExtrFilter` `OrderDual` `OrderDual.instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	—
`isExtrOn_const` 📖	mathematical	—	`IsExtrOn`	—	`isExtrFilter_const`
`isExtrOn_dual_iff` 📖	mathematical	—	`IsExtrOn` `OrderDual` `OrderDual.instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	—
`isMaxFilter_const` 📖	mathematical	—	`IsMaxFilter`	—	`Filter.univ_mem'` `le_rfl`
`isMaxFilter_dual_iff` 📖	mathematical	—	`IsMaxFilter` `OrderDual` `OrderDual.instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `IsMinFilter`	—	—
`isMaxOn_const` 📖	mathematical	—	`IsMaxOn`	—	`isMaxFilter_const`
`isMaxOn_dual_iff` 📖	mathematical	—	`IsMaxOn` `OrderDual` `OrderDual.instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `IsMinOn`	—	—
`isMaxOn_iff` 📖	mathematical	—	`IsMaxOn` `Preorder.toLE`	—	—
`isMaxOn_univ_iff` 📖	mathematical	—	`IsMaxOn` `Set.univ` `Preorder.toLE`	—	`Set.univ_subset_iff` `Set.eq_univ_iff_forall`
`isMinFilter_const` 📖	mathematical	—	`IsMinFilter`	—	`Filter.univ_mem'` `le_rfl`
`isMinFilter_dual_iff` 📖	mathematical	—	`IsMinFilter` `OrderDual` `OrderDual.instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `IsMaxFilter`	—	—
`isMinOn_const` 📖	mathematical	—	`IsMinOn`	—	`isMinFilter_const`
`isMinOn_dual_iff` 📖	mathematical	—	`IsMinOn` `OrderDual` `OrderDual.instPreorder` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `IsMaxOn`	—	—
`isMinOn_iff` 📖	mathematical	—	`IsMinOn` `Preorder.toLE`	—	—
`isMinOn_univ_iff` 📖	mathematical	—	`IsMinOn` `Set.univ` `Preorder.toLE`	—	`Set.univ_subset_iff` `Set.eq_univ_iff_forall`
`sup_eq_of_isMaxOn` 📖	mathematical	`Finset` `SetLike.instMembership` `Finset.instSetLike` `IsMaxOn` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SetLike.coe`	`Finset.sup`	—	`LE.le.antisymm` `Finset.sup_le` `Finset.le_sup`
`sup_eq_of_max` 📖	mathematical	`Set` `Set.instMembership` `Set.range` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Function.invFun` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	`Finset.sup`	—	`Function.apply_invFun_apply` `sup_eq_of_isMaxOn`

---

← Back to Index