Commit 2024-12-06 13:50 e80c9183

View on Github →

chore(Filter/Bases): split (#18450)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

Modified Mathlib/Order/Filter/AtTopBot.lean

deleted theorem Filter.atBot_countable_basis

deleted theorem Filter.atTop_countable_basis

deleted theorem Filter.eventually_iff_seq_eventually

deleted theorem Filter.exists_seq_antitone_tendsto_atTop_atBot

deleted theorem Filter.exists_seq_forall_of_frequently

deleted theorem Filter.exists_seq_monotone_tendsto_atTop_atTop

deleted theorem Filter.exists_seq_tendsto

deleted theorem Filter.frequently_iff_seq_forall

deleted theorem Filter.frequently_iff_seq_frequently

deleted theorem Filter.subseq_tendsto_of_neBot

deleted theorem Filter.tendsto_iff_seq_tendsto

deleted theorem Filter.tendsto_of_seq_tendsto

deleted theorem Filter.tendsto_of_subseq_tendsto

Modified Mathlib/Order/Filter/AtTopBot/Archimedean.lean

Created Mathlib/Order/Filter/AtTopBot/CountablyGenerated.lean

added theorem Filter.atBot_countable_basis

added theorem Filter.atTop_countable_basis

added theorem Filter.eventually_iff_seq_eventually

added theorem Filter.exists_seq_antitone_tendsto_atTop_atBot

added theorem Filter.exists_seq_forall_of_frequently

added theorem Filter.exists_seq_monotone_tendsto_atTop_atTop

added theorem Filter.exists_seq_tendsto

added theorem Filter.frequently_iff_seq_forall

added theorem Filter.frequently_iff_seq_frequently

added theorem Filter.subseq_tendsto_of_neBot

added theorem Filter.tendsto_iff_seq_tendsto

added theorem Filter.tendsto_of_seq_tendsto

added theorem Filter.tendsto_of_subseq_tendsto

Modified Mathlib/Order/Filter/AtTopBot/Field.lean

Modified Mathlib/Order/Filter/Bases.lean

deleted structure Filter.CountableFilterBasis

deleted theorem Filter.HasAntitoneBasis.hasBasis_ge

deleted theorem Filter.HasBasis.exists_antitone_subbasis

deleted theorem Filter.HasBasis.isCountablyGenerated

deleted theorem Filter.HasCountableBasis.isCountablyGenerated

deleted structure Filter.HasCountableBasis

deleted structure Filter.IsCountableBasis

deleted theorem Filter.antitone_seq_of_seq

deleted theorem Filter.countable_biInf_eq_iInf_seq'

deleted theorem Filter.countable_biInf_eq_iInf_seq

deleted theorem Filter.countable_biInf_principal_eq_seq_iInf

deleted theorem Filter.exists_antitone_basis

deleted theorem Filter.exists_antitone_seq

deleted theorem Filter.isCountablyGenerated_biInf_principal

deleted theorem Filter.isCountablyGenerated_bot

deleted theorem Filter.isCountablyGenerated_iff_exists_antitone_basis

deleted theorem Filter.isCountablyGenerated_of_seq

deleted theorem Filter.isCountablyGenerated_principal

deleted theorem Filter.isCountablyGenerated_pure

deleted theorem Filter.isCountablyGenerated_seq

deleted theorem Filter.isCountablyGenerated_top

Modified Mathlib/Order/Filter/Cofinite.lean

Created Mathlib/Order/Filter/CountablyGenerated.lean

added structure Filter.CountableFilterBasis

added theorem Filter.HasAntitoneBasis.hasBasis_ge

added theorem Filter.HasBasis.exists_antitone_subbasis

added theorem Filter.HasBasis.isCountablyGenerated

added theorem Filter.HasCountableBasis.isCountablyGenerated

added structure Filter.HasCountableBasis

added structure Filter.IsCountableBasis

added theorem Filter.antitone_seq_of_seq

added theorem Filter.countable_biInf_eq_iInf_seq'

added theorem Filter.countable_biInf_eq_iInf_seq

added theorem Filter.countable_biInf_principal_eq_seq_iInf

added theorem Filter.exists_antitone_basis

added theorem Filter.exists_antitone_seq

added theorem Filter.isCountablyGenerated_biInf_principal

added theorem Filter.isCountablyGenerated_bot

added theorem Filter.isCountablyGenerated_iff_exists_antitone_basis

added theorem Filter.isCountablyGenerated_of_seq

added theorem Filter.isCountablyGenerated_principal

added theorem Filter.isCountablyGenerated_pure

added theorem Filter.isCountablyGenerated_seq

added theorem Filter.isCountablyGenerated_top

Modified Mathlib/Order/Filter/Defs.lean

added def Filter.pi

Modified Mathlib/Order/Filter/Pi.lean

deleted def Filter.pi

Modified Mathlib/Topology/Bases.lean