Theorems · Definition · general topology
IsMinOn
{α : Type u} → {β : Type v} → [Preorder β] → (α → β) → Set α → α → PropIsMinOn f s a means that f a ≤ f x for all x ∈ s. Note that we do not assume a ∈ s.
- Defined in
- Mathlib.Order.Filter.Extr
- Cited by
- 96 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
- IsMinFilterproof · cited by 36
Cited by96
Results whose statement or proof uses this declaration.
- IsCompact.exists_isMinOnstatement · cited by 15
- IsMinOn.isExtrstatement and proof · cited by 6
- LowerSemicontinuousOn.exists_isMinOnstatement · cited by 6
- IsExtrOn.elimstatement · cited by 5
- isMinOn_iffstatement · cited by 5
- IsCompact.exists_infEDist_eq_edistproof · cited by 3
- Continuous.exists_forall_le'proof · cited by 3
- IsMinOn.localizestatement and proof · cited by 3
- IsMinOn.isLocalMinstatement and proof · cited by 3
- Metric.exists_pos_forall_lt_edistproof · cited by 2
- ConvexOn.isMinOn_of_leftDeriv_nonpos_of_rightDeriv_nonnegstatement · cited by 2
- ContinuousMap.idealOfSet_ofIdeal_eq_closureproof · cited by 2