Commit 2023-02-11 09:23 6ffffa5c

View on Github →

feat: port Data.Analysis.Filter (#1918)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Analysis/Filter.lean

added theorem CFilter.coe_mk

added theorem CFilter.mem_toFilter_sets

added def CFilter.ofEquiv

added theorem CFilter.ofEquiv_val

added def CFilter.toFilter

added structure CFilter

added theorem Filter.Realizer.bot_F

added theorem Filter.Realizer.bot_σ

added theorem Filter.Realizer.le_iff

added theorem Filter.Realizer.map_F

added theorem Filter.Realizer.map_σ

added theorem Filter.Realizer.mem_sets

added theorem Filter.Realizer.ne_bot_iff

added def Filter.Realizer.ofEq

added def Filter.Realizer.ofEquiv

added theorem Filter.Realizer.ofEquiv_F

added theorem Filter.Realizer.ofEquiv_σ

added theorem Filter.Realizer.principal_F

added theorem Filter.Realizer.principal_σ

added theorem Filter.Realizer.tendsto_iff

added theorem Filter.Realizer.top_F

added theorem Filter.Realizer.top_σ

added structure Filter.Realizer