Indexing a net by the members of a filter

A family indexed by the members of a filter l — a net of the shape k : {s : Set α // s ∈ l} → β — is naturally taken along Filter.comap Subtype.val l.smallSets, for which ∀ᶠ s in _, p s says that p holds for every small enough member of l. This file records that this index filter is never the bottom filter, so that convergence along it has content.

theorem TauCeti.comap_val_smallSets_neBot {α : Type u_1} (l : Filter α) : (Filter.comap Subtype.val l.smallSets).NeBot

A filter indexes a nontrivial net by its own members. A net indexed by the members of a filter l converges along this filter, the members read through Filter.smallSets, so that ∀ᶠ s in _, p s says that p holds for every small enough member of l; it is not the bottom filter, every member of l being an index below itself.