Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-17 09:07 e8bdc7fc

View on Github →

feat(order/filter/filter_product): build hyperreals (#801) Construction of filter products, ultraproducts, some instances, hyperreal numbers.

Estimated changes

Modified src/algebra/field.lean

added theorem inv_eq_zero

Created src/data/real/hyperreal.lean

added theorem hyperreal.epsilon_eq_inv_omega

added theorem hyperreal.epsilon_lt_pos

added theorem hyperreal.epsilon_mul_omega

added theorem hyperreal.epsilon_ne_zero

added theorem hyperreal.epsilon_pos

added theorem hyperreal.gt_of_tendsto_zero_of_neg

added def hyperreal.infinitesimal

added theorem hyperreal.infinitesimal_epsilon

added theorem hyperreal.infinitesimal_of_tendsto_zero

added theorem hyperreal.inv_epsilon_eq_omega

added def hyperreal.is_st

added theorem hyperreal.is_st_unique

added theorem hyperreal.lt_of_tendsto_zero_of_pos

added theorem hyperreal.neg_lt_of_tendsto_zero_of_neg

added theorem hyperreal.omega_ne_zero

added theorem hyperreal.omega_pos

added def hyperreal

Modified src/data/real/nnreal.lean

deleted theorem inv_eq_zero

Modified src/data/set/basic.lean

added theorem set.set_of_eq_eq_singleton

Modified src/order/filter/basic.lean

added theorem filter.cofinite_ne_bot

added theorem filter.compl_mem_hyperfilter_of_finite

added theorem filter.hyperfilter_le_cofinite

added theorem filter.is_ultrafilter_hyperfilter

added theorem filter.mem_hyperfilter_of_finite_compl

added theorem filter.nmem_hyperfilter_of_finite

Created src/order/filter/filter_product.lean

added def filter.bigly_equal

added def filter.filter_product.lift

added def filter.filter_product.lift_rel

added def filter.filter_product.lift_rel₂

added def filter.filter_product.lift₂

added theorem filter.filter_product.lt_def'

added theorem filter.filter_product.lt_def

added def filter.filter_product.of

added theorem filter.filter_product.of_add

added theorem filter.filter_product.of_eq

added theorem filter.filter_product.of_eq_coe

added theorem filter.filter_product.of_eq_zero

added theorem filter.filter_product.of_id

added theorem filter.filter_product.of_inj

added theorem filter.filter_product.of_inv

added theorem filter.filter_product.of_le

added theorem filter.filter_product.of_le_of_le

added theorem filter.filter_product.of_lt

added theorem filter.filter_product.of_lt_of_lt

added theorem filter.filter_product.of_mul

added theorem filter.filter_product.of_ne

added theorem filter.filter_product.of_ne_zero

added theorem filter.filter_product.of_neg

added theorem filter.filter_product.of_one

added theorem filter.filter_product.of_rel

added theorem filter.filter_product.of_rel_of_rel

added theorem filter.filter_product.of_rel_of_rel₂

added theorem filter.filter_product.of_rel₂

added def filter.filter_product.of_seq

added theorem filter.filter_product.of_seq_add

added theorem filter.filter_product.of_seq_fun

added theorem filter.filter_product.of_seq_fun₂

added theorem filter.filter_product.of_seq_inv

added theorem filter.filter_product.of_seq_mul

added theorem filter.filter_product.of_seq_neg

added theorem filter.filter_product.of_seq_one

added theorem filter.filter_product.of_seq_zero

added theorem filter.filter_product.of_zero

added def filter.filterprod