Structures · Order
Filter.NeBot
A filter is NeBot if it is not equal to ⊥, or equivalently the empty set does not belong to
the filter. Bourbaki include this assumption in the definition of a filter but we prefer to have a
CompleteLattice structure on Filter _, so we use a typeclass argument in lemmas instead.
- Defined in
- Mathlib.Order.Filter.Defs
- Shape
- One type argument · adds ne'
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances9
- Rat
- ENNReal
- OnePoint
- UpperHalfPlane
- BoxIntegral.TaggedPrepartition
- Prod
- OrderDual
- Set
- Finset
How is a type an instance?
Loading the hierarchy index…
Assumed by484
- Filter.Eventually.exists
- tendsto_nhds_unique
- uniqueDiffOn_univ
- Filter.Eventually.frequently
- Filter.nonempty_of_mem
- le_of_tendsto
- IsClosed.mem_of_tendsto
- ge_of_tendsto
- le_of_tendsto'
- Filter.Frequently.of_forall
- Filter.exists_seq_tendsto
- ge_of_tendsto'
- mem_closure_of_tendsto
- Filter.Tendsto.limUnder_eq
- le_of_tendsto_of_tendsto'
- uniqueDiffWithinAt_univ
- IsOpen.uniqueDiffOn
- Ultrafilter.of
- Ultrafilter.of_le
- Filter.Tendsto.not_tendsto
- Filter.Tendsto.liminf_eq
- tendsto_nhds_unique_of_eventuallyEq
- le_of_tendsto_of_tendsto
- Filter.Tendsto.limsup_eq
- stronglyMeasurable_of_tendsto
- Filter.limsup_const
- nhds_basis_balanced
- tendsto_nhds_unique_inseparable
- not_tendsto_atTop_of_tendsto_nhds
- aestronglyMeasurable_of_tendsto_ae
- mem_tangentConeAt_of_seq
- Filter.liminf_const
- Filter.Tendsto.neBot
- Filter.eventually_const
- Filter.IsBounded.isCobounded_flip
- Filter.NeBot.ne'
- aemeasurable_of_tendsto_metrizable_ae
- Filter.Eventually.exists_gt
- measurable_of_tendsto_metrizable'
- IsOpen.uniqueDiffWithinAt
- TendstoLocallyUniformlyOn.differentiableOn
- ClusterPt.of_le_nhds
- not_tendsto_nhds_of_tendsto_atTop
- ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE
- Filter.compl_notMem
- lim_eq
- MeasureTheory.AECover.integrable_of_integral_norm_bounded
- Filter.IsBoundedUnder.isCoboundedUnder_ge
- not_continuousAt_of_tendsto
- dense_compl_singleton
Ancestors0
No ancestors.