Commit 2024-11-25 09:04 454bc8a1

View on Github →

chore: split Order.Filter.Basic, creating Order.Filter.Finite (#19354)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Order/Filter/Bases.lean

Modified Mathlib/Order/Filter/Basic.lean

deleted theorem Filter.biInter_finset_mem

added theorem Filter.biInter_mem'

deleted theorem Filter.biInter_mem

deleted theorem Filter.eventually_all

deleted theorem Filter.eventually_all_finite

deleted theorem Filter.eventually_all_finset

deleted theorem Filter.eventually_imp_distrib_left

deleted theorem Filter.exists_iInter_of_mem_iInf

deleted theorem Filter.frequently_and_distrib_left

deleted theorem Filter.frequently_and_distrib_right

deleted theorem Filter.iInf_principal'

deleted theorem Filter.iInf_principal

deleted theorem Filter.iInf_principal_finite

deleted theorem Filter.iInf_principal_finset

deleted theorem Filter.iInf_sets_eq_finite'

deleted theorem Filter.iInf_sets_eq_finite

deleted theorem Filter.iInf_sets_induct

added theorem Filter.iInter_mem'

deleted theorem Filter.iInter_mem

deleted theorem Filter.mem_generate_iff

deleted theorem Filter.mem_iInf'

deleted theorem Filter.mem_iInf

deleted theorem Filter.mem_iInf_finite'

deleted theorem Filter.mem_iInf_finite

deleted theorem Filter.mem_iInf_finset

deleted theorem Filter.mem_iInf_of_finite

deleted theorem Filter.mem_iInf_of_iInter

deleted theorem Filter.sInter_mem

deleted theorem Finset.eventuallyEq_iInter

deleted theorem Finset.eventuallyEq_iUnion

deleted theorem Finset.eventuallyLE_iInter

deleted theorem Finset.eventuallyLE_iUnion

deleted theorem Pairwise.exists_mem_filter_of_disjoint

deleted theorem Set.Finite.eventuallyEq_iInter

deleted theorem Set.Finite.eventuallyEq_iUnion

deleted theorem Set.Finite.eventuallyLE_iInter

deleted theorem Set.Finite.eventuallyLE_iUnion

deleted theorem Set.PairwiseDisjoint.exists_mem_filter

Modified Mathlib/Order/Filter/CardinalInter.lean

Modified Mathlib/Order/Filter/Cocardinal.lean

Modified Mathlib/Order/Filter/CountableSeparatingOn.lean

Modified Mathlib/Order/Filter/Extr.lean

Created Mathlib/Order/Filter/Finite.lean

added theorem Filter.biInter_finset_mem

added theorem Filter.biInter_mem

added theorem Filter.eventually_all

added theorem Filter.eventually_all_finite

added theorem Filter.eventually_all_finset

added theorem Filter.eventually_imp_distrib_left

added theorem Filter.exists_iInter_of_mem_iInf

added theorem Filter.frequently_and_distrib_left

added theorem Filter.frequently_and_distrib_right

added theorem Filter.iInf_principal'

added theorem Filter.iInf_principal

added theorem Filter.iInf_principal_finite

added theorem Filter.iInf_principal_finset

added theorem Filter.iInf_sets_eq_finite'

added theorem Filter.iInf_sets_eq_finite

added theorem Filter.iInf_sets_induct

added theorem Filter.iInter_mem

added theorem Filter.mem_generate_iff

added theorem Filter.mem_iInf'

added theorem Filter.mem_iInf

added theorem Filter.mem_iInf_finite'

added theorem Filter.mem_iInf_finite

added theorem Filter.mem_iInf_finset

added theorem Filter.mem_iInf_of_finite

added theorem Filter.mem_iInf_of_iInter

added theorem Filter.sInter_mem

added theorem Finset.eventuallyEq_iInter

added theorem Finset.eventuallyEq_iUnion

added theorem Finset.eventuallyLE_iInter

added theorem Finset.eventuallyLE_iUnion

added theorem Pairwise.exists_mem_filter_of_disjoint

added theorem Set.Finite.eventuallyEq_iInter

added theorem Set.Finite.eventuallyEq_iUnion

added theorem Set.Finite.eventuallyLE_iInter

added theorem Set.Finite.eventuallyLE_iUnion

added theorem Set.PairwiseDisjoint.exists_mem_filter

Modified Mathlib/Order/Filter/Germ/Basic.lean

Modified Mathlib/Order/Filter/Subsingleton.lean

Modified Mathlib/SetTheory/Cardinal/CountableCover.lean