Theorems · Definition · general topology

IsMaxFilter

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

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

Defined in

Mathlib.Order.Filter.Extr

Cited by

38 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

Preorder