Commit 2023-02-19 16:35 3444d0d3

View on Github →

feat: Port/Order.Filter.FilterProduct (#2366) also names instances in Order.Filter.Germ

Estimated changes

added theorem Filter.Germ.abs_def
added theorem Filter.Germ.coe_lt
added theorem Filter.Germ.coe_pos
added theorem Filter.Germ.const_abs
added theorem Filter.Germ.const_inf
added theorem Filter.Germ.const_lt
added theorem Filter.Germ.const_max
added theorem Filter.Germ.const_min
added theorem Filter.Germ.const_sup
added theorem Filter.Germ.lt_def
added theorem Filter.Germ.max_def
added theorem Filter.Germ.min_def