Mathlib Map

Theorems · Theorem · general topology

Filter.IsBasis.nonempty

∀ {α : Type u_1} {ι : Sort u_4} {p : ι → Prop} {s : ι → Set α}, Filter.IsBasis p s → ∃ i, p i

There exists at least one i that satisfies p.

Defined in
Mathlib.Order.Filter.Bases.Basic
Cited by
0 results in Mathlib
Foundations
Depth 2 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Set · cited by 53352SetFilter.IsBasis · cited by 14Filter.IsBasisIsBasis.nonemptyCITED BYCITES

Cites2

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

  • Setstatement and proof · cited by 53,352
  • Filter.IsBasisstatement and proof · cited by 14

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.