Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-29 15:01 eb05a940

View on Github →

feat(order/filter/germ): define filter.germ (#3172) Actually we already had this definition under the name filter_product.

Estimated changes

deleted theorem hyperreal.cast_div
modified theorem hyperreal.coe_abs
added theorem hyperreal.coe_add
added theorem hyperreal.coe_bit0
added theorem hyperreal.coe_bit1
added theorem hyperreal.coe_div
modified theorem hyperreal.coe_eq_coe
added theorem hyperreal.coe_eq_one
added theorem hyperreal.coe_eq_zero
added theorem hyperreal.coe_inv
modified theorem hyperreal.coe_le_coe
modified theorem hyperreal.coe_lt_coe
modified theorem hyperreal.coe_max
modified theorem hyperreal.coe_min
added theorem hyperreal.coe_mul
added theorem hyperreal.coe_neg
added theorem hyperreal.coe_one
added theorem hyperreal.coe_pos
added theorem hyperreal.coe_sub
added theorem hyperreal.coe_zero
modified theorem hyperreal.epsilon_lt_pos
modified def hyperreal.is_st
modified theorem hyperreal.is_st_Sup
modified theorem hyperreal.st_eq_Sup
modified def hyperreal
deleted def filter.bigly_equal
deleted def filter.filterprod
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_div
added theorem filter.germ.const_lt
added theorem filter.germ.const_max
added theorem filter.germ.const_min
added theorem filter.germ.lt_def
added theorem filter.germ.max_def
added theorem filter.germ.min_def
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_one
added theorem filter.germ.coe_smul'
added theorem filter.germ.coe_smul
added theorem filter.germ.coe_sub
added theorem filter.germ.const_bot
added theorem filter.germ.const_inf
added theorem filter.germ.const_inj
added theorem filter.germ.const_le
added theorem filter.germ.const_sup
added theorem filter.germ.const_top
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 theorem filter.germ.mk'_eq_coe
added def filter.germ