Commit 2023-01-24 10:06 5dd5db22

View on Github →

Feat: port Order.Filter.SmallSets (#1810)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Filter/SmallSets.lean

added theorem Filter.HasAntitoneBasis.tendsto_smallSets

added theorem Filter.HasBasis.smallSets

added theorem Filter.Tendsto.of_smallSets

added theorem Filter.Tendsto.smallSets_mono

added theorem Filter.comap_smallSets

added theorem Filter.eventually_smallSets

added theorem Filter.eventually_smallSets_eventually

added theorem Filter.eventually_smallSets_forall

added theorem Filter.eventually_smallSets_subset

added theorem Filter.eventually_small_sets'

added theorem Filter.frequently_smallSets

added theorem Filter.frequently_smallSets_mem

added theorem Filter.hasBasis_smallSets

added theorem Filter.monotone_smallSets

added def Filter.smallSets

added theorem Filter.smallSets_bot

added theorem Filter.smallSets_comap

added theorem Filter.smallSets_eq_generate

added theorem Filter.smallSets_inf

added theorem Filter.smallSets_infᵢ

added theorem Filter.smallSets_principal

added theorem Filter.smallSets_top

added theorem Filter.tendsto_smallSets_iff