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 ofFilterBases
,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 splitsAddTopBot/Basic.lean
further, moving out finiteness toAtTopBot/Finite.lean
and upstreaming results on products toAtTopBot/Prod.lean
. This should hopefully reduce the amount of finiteness that is needed to work with topological and metric spaces.