Commit 2024-04-03 22:32 beeea28f

View on Github →

feat : new properties of the CardinalInterFilter (#11758) extend more of the API from CountableInterFilter to CardinalInterFilter

Estimated changes

Modified Mathlib/Order/Filter/CardinalInter.lean

deleted theorem CardinalInterFilter.of_CardinalInterFilter_of_lt

added theorem CardinalInterFilter.of_cardinalInterFilter_of_le

added theorem CardinalInterFilter.of_cardinalInterFilter_of_lt

added inductive Filter.CardinalGenerateSets

added def Filter.cardinalGenerate

added theorem Filter.cardinalGenerate_isGreatest

added theorem Filter.cardinalInter_ofCardinalGenerate

added theorem Filter.le_cardinalGenerate_iff_of_cardinalInterFilter

added theorem Filter.mem_cardinaleGenerate_iff

added theorem Filter.mem_ofCardinalInter

added theorem Filter.mem_ofCardinalUnion

added def Filter.ofCardinalInter

added def Filter.ofCardinalUnion

Modified Mathlib/Order/Filter/CountableInter.lean

modified theorem Filter.mem_ofCountableUnion

modified def Filter.ofCountableUnion

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

added theorem Cardinal.IsRegular.nat_lt

added theorem Cardinal.card_biUnion_lt_iff_forall_of_isRegular

added theorem Cardinal.card_iUnion_lt_iff_forall_of_isRegular

added theorem Cardinal.card_lt_of_card_biUnion_lt

added theorem Cardinal.card_lt_of_card_iUnion_lt