Theorems · Definition · general topology
IsExtrOn
{α : Type u} → {β : Type v} → [Preorder β] → (α → β) → Set α → α → PropIsExtrOn f s a means IsMinOn f s a or IsMaxOn f s a
- Defined in
- Mathlib.Order.Filter.Extr
- Cited by
- 30 results in Mathlib
- Foundations
- Depth 8 from the axioms · uses no axioms
- Assumes
- Preorder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Preorderstatement and proof · cited by 7,952
- Filter.principalproof · cited by 740
- IsExtrFilterproof · cited by 16
Cited by30
Results whose statement or proof uses this declaration.
- IsMaxOn.isExtrstatement · cited by 6
- IsMinOn.isExtrstatement · cited by 6
- IsExtrOn.elimstatement · cited by 5
- exists_isLocalExtr_Iooproof · cited by 3
- IsExtrOn.hasLineDerivAt_eq_zerostatement and proof · cited by 3
- IsExtrOn.hasLineDerivWithinAt_eq_zerostatement and proof · cited by 3
- IsExtrOn.isLocalExtrstatement and proof · cited by 3
- IsExtrOn.on_subsetstatement and proof · cited by 3
- exists_Ioo_extr_on_Iccstatement · cited by 3
- IsExtrOn.lineDerivWithin_eq_zerostatement and proof · cited by 2
- IsExtrOn.lineDeriv_eq_zerostatement and proof · cited by 2
- isExtrOn_dual_iffstatement · cited by 2