Commit 2023-07-26 09:26 6b4ff5d9

View on Github →

feat(Filter/Germ): review algebraic instances (#6130) Motivated by the Sphere Eversion Project.

Estimated changes

deleted theorem Filter.Germ.const_inf
deleted theorem Filter.Germ.const_sup
added theorem Filter.Germ.coe_int
added theorem Filter.Germ.coe_nat
added theorem Filter.Germ.coe_ofNat
added theorem Filter.Germ.const_inf
added theorem Filter.Germ.const_nat
added theorem Filter.Germ.const_sup