Commit 2025-03-05 12:47 815573cf

View on Github →

chore(Order/Filter): split Filter/Bases.lean (#21784) The goal of this PR is to move the requirement for finiteness further down the import graph. To do so, this PR splits Filter/Bases.lean into three files:

  • Bases/Defs.lean: definition of FilterBases, IsFilterBasis, Filter.HasBasis
  • Bases/Basic.lean: basic results (those do not depend on finiteness)
  • Bases/Finite.lean: results that depend on finiteness We then use this split to splits AddTopBot/Basic.lean further, moving out finiteness to AtTopBot/Finite.lean and upstreaming results on products to AtTopBot/Prod.lean. This should hopefully reduce the amount of finiteness that is needed to work with topological and metric spaces.

Estimated changes

deleted theorem Filter.high_scores
deleted theorem Filter.low_scores
added theorem Filter.high_scores
added theorem Filter.low_scores
deleted theorem Filter.generate_neBot_iff
deleted theorem Filter.hasBasis_generate
deleted theorem Filter.hasBasis_iInf'
deleted theorem Filter.hasBasis_iInf
added theorem Filter.hasBasis_iInf'
added theorem Filter.hasBasis_iInf