Commit 2021-06-18 18:18 52dbff0f

View on Github →

chore(topology/basic): rename compact_Icc to is_compact_Icc (#7979) Also rename compact_interval to is_compact_interval. And a bunch of random additions, all minor, as prerequisistes to #7978

Estimated changes

Modified archive/100-theorems-list/9_area_of_a_circle.lean

Modified src/analysis/calculus/darboux.lean

Modified src/analysis/calculus/local_extr.lean

Modified src/analysis/normed_space/basic.lean

added theorem bounded_iff_forall_norm_le

added theorem is_compact.exists_bound_of_continuous_on

Modified src/analysis/normed_space/dual.lean

added theorem normed_space.eq_iff_forall_dual_eq

added theorem normed_space.eq_zero_iff_forall_dual_eq_zero

Modified src/analysis/normed_space/hahn_banach.lean

added theorem norm'_eq_zero_iff

Modified src/data/real/ereal.lean

added theorem ereal.coe_to_real

added theorem ereal.lt_iff_exists_real_btwn

Modified src/data/real/liouville.lean

Modified src/dynamics/circle/rotation_number/translation_number.lean

Modified src/measure_theory/borel_space.lean

Modified src/measure_theory/haar_measure.lean

Modified src/measure_theory/integrable_on.lean

added theorem continuous.integrable_on_Icc

added theorem continuous.integrable_on_interval

deleted theorem continuous_linear_map.integrable_comp

added theorem continuous_on.integrable_on_Icc

added theorem continuous_on.integrable_on_interval

added theorem measure_theory.integrable_on.continuous_on_mul

added theorem measure_theory.integrable_on.mul_continuous_on

added theorem measure_theory.integrable_on_singleton_iff

Modified src/measure_theory/interval_integral.lean

Modified src/measure_theory/l1_space.lean

added theorem continuous_linear_map.integrable_comp

Modified src/measure_theory/lebesgue_measure.lean

Modified src/measure_theory/measure_space.lean

modified theorem measure_theory.ae_restrict_iff'

added theorem measure_theory.ae_restrict_mem

Modified src/topology/algebra/ordered/basic.lean

deleted theorem compact_Icc

deleted theorem compact_interval

deleted theorem compact_pi_Icc

added theorem is_compact_Icc

added theorem is_compact_interval

added theorem is_compact_pi_Icc

Modified src/topology/instances/real.lean

Modified src/topology/metric_space/basic.lean

Modified src/topology/metric_space/gromov_hausdorff_realized.lean

Modified test/monotonicity.lean