Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-21 22:05 b3fc8013

View on Github →

refactor(data/real/nnreal): derive order structure for ennreal from with_top nnreal

Estimated changes

Modified algebra/ordered_group.lean

added theorem le_add_left

added theorem le_add_right

deleted theorem with_bot.bot_lt_some

deleted theorem with_bot.coe_lt_coe

added theorem with_top.add_eq_top

added theorem with_top.add_lt_add_iff_left

deleted theorem with_top.coe_ne_top

deleted theorem with_top.top_ne_coe

added theorem with_top.zero_lt_coe

added theorem with_top.zero_lt_top

Modified algebra/ordered_ring.lean

modified theorem mul_le_one

deleted theorem option.bind_comm

added theorem with_top.coe_mul

deleted theorem with_top.coe_mul_coe

deleted theorem with_top.none_eq_top

deleted theorem with_top.some_eq_coe

added theorem with_top.top_mul_top

Modified analysis/ennreal.lean

deleted theorem ennreal.Inf_add

deleted theorem ennreal.add_infi

deleted theorem ennreal.coe_eq_coe

added theorem ennreal.coe_image_univ_mem_nhds

deleted theorem ennreal.coe_mul

added theorem ennreal.coe_nat

deleted theorem ennreal.coe_one

added theorem ennreal.continuous_coe

deleted theorem ennreal.continuous_of_real

added theorem ennreal.embedding_coe

deleted theorem ennreal.exists_pos_sum_of_encodable

deleted theorem ennreal.infi_add

deleted theorem ennreal.infi_add_infi

deleted theorem ennreal.infi_of_real

deleted theorem ennreal.infi_sum

added theorem ennreal.is_open_ne_top

added theorem ennreal.nhds_coe

added theorem ennreal.nhds_coe_coe

deleted theorem ennreal.nhds_of_real_eq_map_of_real_nhds

deleted theorem ennreal.nhds_of_real_eq_map_of_real_nhds_nonneg

deleted theorem ennreal.sub_infi

modified theorem ennreal.sub_supr

deleted theorem ennreal.supr_of_real

added theorem ennreal.tendsto_coe

deleted theorem ennreal.tendsto_coe_iff

added theorem ennreal.tendsto_nhds_top

deleted theorem ennreal.tendsto_of_ennreal

deleted theorem ennreal.tendsto_of_real

deleted theorem ennreal.tendsto_of_real_iff

added theorem ennreal.tendsto_to_nnreal

modified theorem has_sum_of_nonneg_of_le

added theorem nnreal.exists_le_is_sum_of_le

modified theorem nnreal.has_sum_of_le

added theorem topological_space.nhds_swap

added theorem topological_space.prod_mem_nhds_sets

added theorem topological_space.tendsto_nhds_generate_from

added theorem topological_space.tendsto_prod_mk_nhds

Modified analysis/limits.lean

added theorem ennreal.exists_pos_sum_of_encodable

added theorem nnreal.exists_pos_sum_of_encodable

Modified analysis/measure_theory/lebesgue_measure.lean

Modified analysis/measure_theory/measure_space.lean

Modified analysis/measure_theory/outer_measure.lean

Modified analysis/nnreal.lean

added theorem nnreal.continuous_coe

added theorem nnreal.continuous_of_real

added theorem nnreal.tendsto_of_real

added theorem nnreal.tendsto_sub

added theorem nnreal.tsum_coe

Modified analysis/probability_mass_function.lean

Modified analysis/topology/continuity.lean

modified theorem embedding.tendsto_nhds_iff

Modified data/option.lean

added theorem option.bind_comm

Modified data/real/basic.lean

added theorem real.Inf_empty

added theorem real.Inf_of_not_bdd_below

added theorem real.Sup_empty

added theorem real.Sup_of_not_bdd_above

modified def real.of_rat

Modified data/real/ennreal.lean

added theorem ennreal.Inf_add

added theorem ennreal.add_eq_top

added theorem ennreal.add_infi

deleted theorem ennreal.add_infty

added theorem ennreal.add_lt_add_iff_left

modified theorem ennreal.add_sub_self

added theorem ennreal.add_top

added theorem ennreal.bot_eq_zero

added theorem ennreal.coe_Inf

added theorem ennreal.coe_Sup

added theorem ennreal.coe_add

added theorem ennreal.coe_eq_coe

added theorem ennreal.coe_eq_one

added theorem ennreal.coe_eq_zero

added theorem ennreal.coe_finset_prod

added theorem ennreal.coe_finset_sum

added theorem ennreal.coe_le_coe

added theorem ennreal.coe_le_iff

added theorem ennreal.coe_le_one_iff

added theorem ennreal.coe_lt_coe

added theorem ennreal.coe_lt_one_iff

added theorem ennreal.coe_lt_top

added theorem ennreal.coe_mem_upper_bounds

added theorem ennreal.coe_mul

added theorem ennreal.coe_ne_top

added theorem ennreal.coe_one

added theorem ennreal.coe_sub

added theorem ennreal.coe_to_nnreal

added theorem ennreal.coe_zero

added theorem ennreal.div_def

added theorem ennreal.div_le_iff_le_mul

modified theorem ennreal.forall_ennreal

added theorem ennreal.infi_add

added theorem ennreal.infi_add_infi

added theorem ennreal.infi_sum

deleted theorem ennreal.infty_add

deleted theorem ennreal.infty_le_iff

deleted theorem ennreal.infty_mem_upper_bounds

deleted theorem ennreal.infty_mul

deleted theorem ennreal.infty_mul_of_real

deleted theorem ennreal.infty_ne_of_real

deleted theorem ennreal.infty_ne_zero

deleted theorem ennreal.infty_sub_of_real

added theorem ennreal.inv_coe

added theorem ennreal.inv_eq_top

added theorem ennreal.inv_eq_zero

deleted theorem ennreal.inv_infty

modified theorem ennreal.inv_inv

added theorem ennreal.inv_le_iff_le_mul

added theorem ennreal.inv_ne_top

added theorem ennreal.inv_ne_zero

deleted theorem ennreal.inv_of_real

added theorem ennreal.inv_top

deleted theorem ennreal.is_lub_of_real

deleted theorem ennreal.le_add_left

deleted theorem ennreal.le_add_right

added theorem ennreal.le_coe_iff

deleted theorem ennreal.le_def

added theorem ennreal.le_div_iff_mul_le

deleted theorem ennreal.le_infty

added theorem ennreal.le_inv_iff_mul_le

modified theorem ennreal.le_of_forall_epsilon_le

deleted theorem ennreal.le_of_real_iff

deleted theorem ennreal.le_zero_iff_eq

modified theorem ennreal.lt_add_right

added theorem ennreal.lt_iff_exists_coe

deleted theorem ennreal.lt_iff_exists_of_real

added theorem ennreal.mul_eq_mul_left

deleted theorem ennreal.mul_infty

deleted theorem ennreal.mul_le_mul

added theorem ennreal.mul_le_mul_left

added theorem ennreal.mul_top

added theorem ennreal.none_eq_top

deleted theorem ennreal.not_infty_lt

modified theorem ennreal.not_lt_zero

added theorem ennreal.not_top_le_coe

deleted def ennreal.of_ennreal

deleted theorem ennreal.of_ennreal_of_real

deleted theorem ennreal.of_nonneg_real_eq_of_real

deleted def ennreal.of_real

deleted theorem ennreal.of_real_add

deleted theorem ennreal.of_real_add_le

deleted theorem ennreal.of_real_eq_of_real_of

deleted theorem ennreal.of_real_eq_one_iff

deleted theorem ennreal.of_real_eq_zero_iff

deleted theorem ennreal.of_real_le_of_real

deleted theorem ennreal.of_real_le_of_real_iff

deleted theorem ennreal.of_real_lt_infty

deleted theorem ennreal.of_real_lt_of_real_iff

deleted theorem ennreal.of_real_lt_of_real_iff_cases

deleted theorem ennreal.of_real_mem_upper_bounds

deleted theorem ennreal.of_real_mul_infty

deleted theorem ennreal.of_real_mul_of_real

deleted theorem ennreal.of_real_ne_infty

deleted theorem ennreal.of_real_ne_of_real_of

deleted theorem ennreal.of_real_of_ennreal

deleted theorem ennreal.of_real_of_nonpos

deleted theorem ennreal.of_real_of_not_nonneg

deleted theorem ennreal.of_real_one

deleted theorem ennreal.of_real_sub_of_real

deleted theorem ennreal.of_real_zero

added theorem ennreal.one_eq_coe

deleted theorem ennreal.one_eq_of_real_iff

added theorem ennreal.one_le_coe_iff

deleted theorem ennreal.one_le_of_real_iff

added theorem ennreal.one_lt_zero_iff

added theorem ennreal.one_ne_top

added theorem ennreal.some_eq_coe

modified theorem ennreal.sub_add_cancel_of_le

added theorem ennreal.sub_infi

deleted theorem ennreal.sum_of_real

added theorem ennreal.supr_sub

added theorem ennreal.to_nnreal_coe

added theorem ennreal.top_add

added theorem ennreal.top_mem_upper_bounds

added theorem ennreal.top_mul

added theorem ennreal.top_mul_top

added theorem ennreal.top_ne_coe

added theorem ennreal.top_ne_one

added theorem ennreal.top_ne_zero

added theorem ennreal.top_sub_coe

added theorem ennreal.top_to_nnreal

added theorem ennreal.zero_eq_coe

deleted theorem ennreal.zero_eq_of_real_iff

deleted theorem ennreal.zero_le_of_ennreal

added theorem ennreal.zero_lt_coe_iff

deleted theorem ennreal.zero_lt_of_real_iff

deleted theorem ennreal.zero_ne_infty

added theorem ennreal.zero_ne_top

Modified data/real/nnreal.lean

added theorem inv_eq_zero

added theorem nnreal.add_sub_cancel'

added theorem nnreal.add_sub_cancel

added theorem nnreal.bdd_above_coe

added theorem nnreal.bdd_below_coe

added theorem nnreal.coe_Inf

added theorem nnreal.coe_Sup

added theorem nnreal.coe_of_real

added theorem nnreal.div_def

added theorem nnreal.inv_eq_zero

added theorem nnreal.inv_inv

added theorem nnreal.inv_le

added theorem nnreal.inv_le_of_le_mul

added theorem nnreal.inv_mul_cancel

added theorem nnreal.inv_pos

added theorem nnreal.inv_zero

added theorem nnreal.le_inv_iff_mul_le

added theorem nnreal.le_of_forall_epsilon_le

added theorem nnreal.lt_iff_exists_rat_btwn

added theorem nnreal.mul_eq_mul_left

added theorem nnreal.mul_inv_cancel

added theorem nnreal.of_real_add_le

added theorem nnreal.of_real_add_of_real

added theorem nnreal.of_real_coe

added theorem nnreal.of_real_le_of_real

added theorem nnreal.of_real_le_of_real_iff

added theorem nnreal.of_real_of_nonpos

added theorem nnreal.of_real_zero

added theorem nnreal.prod_coe

added theorem nnreal.smul_coe

added theorem nnreal.sub_add_cancel_of_le

added theorem nnreal.sub_eq_zero

added theorem nnreal.sub_le_iff_le_add

modified theorem nnreal.sum_coe

added theorem nnreal.zero_le_coe

added theorem nnreal.zero_lt_of_real

added theorem set.image_eq_empty

Modified order/bounded_lattice.lean

added theorem with_bot.bot_lt_coe

added theorem with_bot.bot_lt_some

added theorem with_bot.coe_eq_coe

added theorem with_bot.coe_lt_coe

added theorem with_bot.none_eq_bot

added theorem with_bot.some_eq_coe

added theorem with_top.coe_eq_coe

added theorem with_top.coe_le_iff

added theorem with_top.coe_lt_coe

added theorem with_top.coe_lt_top

added theorem with_top.coe_ne_top

added theorem with_top.le_coe_iff

added theorem with_top.lt_iff_exists_coe

added theorem with_top.none_eq_top

added theorem with_top.not_top_le_coe

added theorem with_top.some_eq_coe

added theorem with_top.top_ne_coe

Modified order/conditionally_complete_lattice.lean

deleted theorem bdd_above_bot

added theorem bdd_below_bot

added theorem lattice.cSup_empty

added theorem with_top.coe_Inf

added theorem with_top.coe_Sup

added theorem with_top.has_glb

added theorem with_top.has_lub

added theorem with_top.is_glb_Inf

added theorem with_top.is_lub_Sup

Modified order/filter.lean

added theorem filter.tendsto_map'_iff

Modified order/galois_connection.lean