Theorems · Definition · general topology
IsMaxOn
{α : Type u} → {β : Type v} → [Preorder β] → (α → β) → Set α → α → PropIsMaxOn f s a means that f x ≤ f a for all x ∈ s. Note that we do not assume a ∈ s.
- Defined in
- Mathlib.Order.Filter.Extr
- Cited by
- 114 results in Mathlib
- Foundations
- Depth 8 from the axioms, rests on 27 definitions · 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
- IsMaxFilterproof · cited by 38
Cited by114
Results whose statement or proof uses this declaration.
- IsCompact.exists_isMaxOnstatement · cited by 22
- IsMaxOn.isExtrstatement and proof · cited by 6
- isMaxOn_iffstatement · cited by 6
- geometric_hahn_banach_compact_closedproof · cited by 5
- IsExtrOn.elimstatement · cited by 5
- IsMaxOn.isLocalMaxstatement and proof · cited by 4
- IsMaxOn.norm_add_selfstatement and proof · cited by 4
- Complex.norm_eqOn_of_isPreconnected_of_isMaxOnstatement and proof · cited by 3
- Complex.norm_eq_norm_of_isMaxOn_of_ball_subsetstatement and proof · cited by 3
- IsMaxOn.closurestatement and proof · cited by 3
- IsMaxOn.on_subsetstatement and proof · cited by 3
- spectrum.exists_nnnorm_eq_spectralRadius_of_nonemptyproof · cited by 3