Mathlib.Order.Filter.Ker._auxLemma.1

theorem Mathlib.Order.Filter.Ker._auxLemma.1 : ∀ {α : Type u_2} {f : Filter α} {a : α}, (a ∈ f.ker) = ∀ s ∈ f, a ∈ s

This theorem states that for any type `α`, any filter `f` on `α`, and any element `a` of `α`, `a` is in the kernel of `f` if and only if `a` is in every set `s` in `f`. In other words, an element belongs to the kernel of a filter precisely when it belongs to every set that the filter contains.

More concisely: An element belongs to the kernel of a filter if and only if it is an element of every set in the filter.