Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-31 21:28 233eb660

View on Github →

feat(data/real/ennreal): more on integer powers on ennreal (#10071)

Estimated changes

Modified src/algebra/group_power/basic.lean

added theorem zpow_two

Modified src/algebra/order/archimedean.lean

added theorem exists_mem_Ico_zpow

added theorem exists_mem_Ioc_zpow

deleted theorem exists_zpow_near'

deleted theorem exists_zpow_near

Modified src/analysis/normed_space/basic.lean

Modified src/data/real/ennreal.lean

added theorem ennreal.Ioo_zero_top_eq_Union_Ico_zpow

added theorem ennreal.add_div

added theorem ennreal.coe_zpow

added theorem ennreal.exists_mem_Ico_zpow

added theorem ennreal.exists_mem_Ioc_zpow

added theorem ennreal.monotone_zpow

added theorem ennreal.one_le_pow_of_one_le

added theorem ennreal.zpow_add

added theorem ennreal.zpow_le_of_le

added theorem ennreal.zpow_lt_top

added theorem ennreal.zpow_pos

Modified src/data/real/nnreal.lean

added theorem nnreal.coe_zpow

added theorem nnreal.exists_mem_Ico_zpow

added theorem nnreal.exists_mem_Ioc_zpow

added theorem nnreal.inv_lt_one

added theorem nnreal.inv_lt_one_iff

added theorem nnreal.zpow_pos

Modified src/topology/instances/ennreal.lean

added theorem ennreal.continuous_pow