Mathlib Map

Theorems · Theorem · general topology

Filter.forall_mem_nonempty_iff_neBot

∀ {α : Type u} {f : Filter α}, (∀ s ∈ f, s.Nonempty) ↔ f.NeBot
Defined in
Mathlib.Order.Filter.Basic
Cited by
4 results in Mathlib
Foundations
Depth 53 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Monotone.leftLim_le · cited by 13Monotone.leftLim_lele_nhds_of_cauchy_adhp · cited by 6le_nhds_of_cauchy_adhpFilter.HasBasis.neBot_iff · cited by 5HasBasis.neBot_iffLaurentSeries.Cauchy.exists_lb_eventual_support · cited by 2Cauchy.exists_lb_eventual…Set · cited by 53352SetFilter · cited by 8121FilterBot.bot · cited by 4720Bot.botSet.Nonempty · cited by 2627Set.NonemptyFilter.NeBot · cited by 853Filter.NeBotFilter.nonempty_of_mem · cited by 36Filter.nonempty_of_memFilter.mem_bot · cited by 7Filter.mem_botSet.not_nonempty_empty · cited by 5Set.not_nonempty_emptyFilter.forall_mem_nonempty_if…CITED BYCITES

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by4

Results whose statement or proof uses this declaration.