Theorems · Theorem · general topology

isMinFilter_const

∀ {α : Type u} {β : Type v} [inst : Preorder β] {l : Filter α} {a : α} {b : β}, IsMinFilter (fun x => b) l a

Defined in

Mathlib.Order.Filter.Extr

Cited by

4 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms

Assumes

Preorder