Commit 2023-02-15 08:14 c8bff08c

View on Github →

feat: port Order.Filter.Germ (#1799)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Filter/Germ.lean

added theorem Filter.EventuallyEq.comp_tendsto

added def Filter.Germ.LiftPred

added def Filter.Germ.LiftRel

added def Filter.Germ.coeMulHom

added def Filter.Germ.coeRingHom

added theorem Filter.Germ.coe_coeMulHom

added theorem Filter.Germ.coe_coeRingHom

added theorem Filter.Germ.coe_compTendsto'

added theorem Filter.Germ.coe_compTendsto

added theorem Filter.Germ.coe_div

added theorem Filter.Germ.coe_eq

added theorem Filter.Germ.coe_inv

added theorem Filter.Germ.coe_le

added theorem Filter.Germ.coe_mul

added theorem Filter.Germ.coe_nonneg

added theorem Filter.Germ.coe_one

added theorem Filter.Germ.coe_pow

added theorem Filter.Germ.coe_smul'

added theorem Filter.Germ.coe_smul

added theorem Filter.Germ.coe_tendsto

added def Filter.Germ.compTendsto'

added theorem Filter.Germ.compTendsto'_coe

added def Filter.Germ.compTendsto

added def Filter.Germ.const

added theorem Filter.Germ.const_bot

added theorem Filter.Germ.const_compTendsto'

added theorem Filter.Germ.const_compTendsto

added theorem Filter.Germ.const_div

added theorem Filter.Germ.const_inj

added theorem Filter.Germ.const_inv

added theorem Filter.Germ.const_le

added theorem Filter.Germ.const_le_iff

added theorem Filter.Germ.const_pow

added theorem Filter.Germ.const_smul

added theorem Filter.Germ.const_top

added theorem Filter.Germ.inductionOn

added theorem Filter.Germ.inductionOn₂

added theorem Filter.Germ.inductionOn₃

added theorem Filter.Germ.le_def

added def Filter.Germ.liftOn

added theorem Filter.Germ.liftPred_coe

added theorem Filter.Germ.liftPred_const

added theorem Filter.Germ.liftPred_const_iff

added theorem Filter.Germ.liftRel_coe

added theorem Filter.Germ.liftRel_const

added theorem Filter.Germ.liftRel_const_iff

added def Filter.Germ.map'

added theorem Filter.Germ.map'_coe

added def Filter.Germ.map

added theorem Filter.Germ.map_coe

added theorem Filter.Germ.map_const

added theorem Filter.Germ.map_id

added theorem Filter.Germ.map_map

added def Filter.Germ.map₂

added theorem Filter.Germ.map₂_coe

added theorem Filter.Germ.map₂_const

added theorem Filter.Germ.mk'_eq_coe

added def Filter.Germ.ofFun

added theorem Filter.Germ.quot_mk_eq_coe

added def Filter.Germ

added def Filter.Product

added theorem Filter.const_eventuallyEq'

added theorem Filter.const_eventuallyEq

added def Filter.germSetoid

added def Filter.productSetoid