Theorems · Definition · general topology

IsMinFilter

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

IsMinFilter f l a means that f a ≤ f x for all x in some l-neighborhood of a

Defined in

Mathlib.Order.Filter.Extr

Cited by

36 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

Preorder