Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-10 13:58 90755c36

View on Github →

refactor(order/filter/ultrafilter): drop filter.is_ultrafilter (#5264) Use bundled ultrafilters instead.

Estimated changes

modified theorem hyperreal.coe_abs
modified theorem hyperreal.coe_lt_coe
modified theorem hyperreal.coe_max
modified theorem hyperreal.coe_min
modified def hyperreal
added theorem filter.empty_nmem_sets
modified theorem filter.principal_ne_bot_iff
modified theorem filter.germ.abs_def
modified theorem filter.germ.coe_lt
modified theorem filter.germ.coe_pos
modified theorem filter.germ.const_abs
modified theorem filter.germ.const_div
modified theorem filter.germ.const_lt
modified theorem filter.germ.const_max
modified theorem filter.germ.const_min
deleted theorem filter.germ.le_def
modified theorem filter.germ.lt_def
modified theorem filter.germ.max_def
modified theorem filter.germ.min_def
added theorem filter.germ.le_def
modified theorem filter.bot_ne_hyperfilter
deleted theorem filter.exists_ultrafilter
deleted theorem filter.hyperfilter_ne_bot
deleted theorem filter.is_ultrafilter.em
modified theorem filter.le_iff_ultrafilter
deleted theorem filter.le_of_ultrafilter
modified theorem filter.mem_iff_ultrafilter
deleted def filter.ultrafilter
deleted theorem filter.ultrafilter_bind
deleted theorem filter.ultrafilter_map
deleted theorem filter.ultrafilter_of_le
deleted theorem filter.ultrafilter_pure
added def ultrafilter.bind
added theorem ultrafilter.coe_inj
added theorem ultrafilter.coe_le_coe
added theorem ultrafilter.coe_map
added theorem ultrafilter.exists_le
added theorem ultrafilter.ext
added def ultrafilter.map
added theorem ultrafilter.mem_coe
added theorem ultrafilter.mem_map
added theorem ultrafilter.of_coe
added theorem ultrafilter.of_le
added theorem ultrafilter.unique
added structure ultrafilter
added def ultrafilter.Lim
modified theorem convergent_eqv_pure
modified theorem ultrafilter_comap_pure_nhds