Theorems · Definition · general topology

IsLocalMinOn

{α : Type u} → {β : Type v} → [TopologicalSpace α] → [Preorder β] → (α → β) → Set α → α → Prop

IsLocalMinOn f s a means that f a ≤ f x for all x ∈ s in some neighborhood of a.

Defined in

Mathlib.Topology.Order.LocalExtr

Cited by

38 results in Mathlib

Foundations

Depth 49 from the axioms · uses propext, Quot.sound

Assumes

TopologicalSpacePreorder