Mathlib Map

Theorems · Theorem · general topology

Filter.filter_eq

∀ {α : Type u_1} {f g : Filter α}, f.sets = g.sets → f = g
Defined in
Mathlib.Order.Filter.Defs
Cited by
6 results in Mathlib
Foundations
Depth 10 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Filter.ext · cited by 60Filter.extFilter.map_id · cited by 22Filter.map_idFilter.map_compose · cited by 3Filter.map_composeFilter.rmap_rmap · cited by 1Filter.rmap_rmapFilter.rcomap_rcomap · cited by 1Filter.rcomap_rcomapFilter.filter_eq_iff · cited by 0Filter.filter_eq_iffSet · cited by 53352SetFilter · cited by 8121FilterSet.univ · cited by 3945Set.univFilter.sets · cited by 56Filter.setsFilter.filter_eqCITED BYCITES

Cites4

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
  • Filterstatement and proof · cited by 8,121
  • Set.univproof · cited by 3,945
  • Filter.setsstatement and proof · cited by 56

Cited by6

Results whose statement or proof uses this declaration.