Theorems · Definition · general topology

IsLocalMaxOn

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

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

Defined in

Mathlib.Topology.Order.LocalExtr

Cited by

39 results in Mathlib

Foundations

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

Assumes

TopologicalSpacePreorder