Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-16 13:55 461865b2

View on Github →

refactor(data/real): move real.sqrt to data.real.sqrt, more dependencies (#5359)

  • define nnreal.sqrt;
  • use general theory to prove that the inverse exists, and is an order_iso;
  • deduce continuity of sqrt from continuity of order_iso.

Estimated changes

deleted theorem real.continuous_sqrt
deleted theorem real.le_sqrt'
deleted theorem real.le_sqrt
deleted theorem real.le_sqrt_of_sqr_le
deleted theorem real.mul_self_sqrt
deleted theorem real.sqr_sqrt
deleted def real.sqrt_aux
deleted theorem real.sqrt_aux_nonneg
deleted theorem real.sqrt_div
deleted theorem real.sqrt_eq_iff_sqr_eq
deleted theorem real.sqrt_eq_zero'
deleted theorem real.sqrt_eq_zero
deleted theorem real.sqrt_exists
deleted theorem real.sqrt_inj
deleted theorem real.sqrt_inv
deleted theorem real.sqrt_le
deleted theorem real.sqrt_le_left
deleted theorem real.sqrt_le_sqrt
deleted theorem real.sqrt_lt
deleted theorem real.sqrt_mul'
deleted theorem real.sqrt_mul
deleted theorem real.sqrt_mul_self
deleted theorem real.sqrt_mul_self_eq_abs
deleted theorem real.sqrt_nonneg
deleted theorem real.sqrt_one
deleted theorem real.sqrt_pos
deleted theorem real.sqrt_prop
deleted theorem real.sqrt_sqr
deleted theorem real.sqrt_sqr_eq_abs
deleted theorem real.sqrt_zero
added theorem continuous.sqrt
added theorem continuous_at.sqrt
added theorem continuous_on.sqrt
added theorem filter.tendsto.sqrt
added theorem nnreal.continuous_sqrt
added theorem nnreal.le_sqrt_iff
added theorem nnreal.mul_sqrt_self
added theorem nnreal.sqrt_div
added theorem nnreal.sqrt_eq_zero
added theorem nnreal.sqrt_inv
added theorem nnreal.sqrt_le_iff
added theorem nnreal.sqrt_mul
added theorem nnreal.sqrt_mul_self
added theorem nnreal.sqrt_one
added theorem nnreal.sqrt_zero
added theorem real.continuous_sqrt
added theorem real.le_sqrt'
added theorem real.le_sqrt
added theorem real.le_sqrt_of_sqr_le
added theorem real.mul_self_sqrt
added theorem real.sqr_sqrt
added def real.sqrt_aux
added theorem real.sqrt_aux_nonneg
added theorem real.sqrt_div
added theorem real.sqrt_eq_zero'
added theorem real.sqrt_eq_zero
added theorem real.sqrt_inj
added theorem real.sqrt_inv
added theorem real.sqrt_le
added theorem real.sqrt_le_iff
added theorem real.sqrt_le_left
added theorem real.sqrt_le_sqrt
added theorem real.sqrt_lt
added theorem real.sqrt_mul'
added theorem real.sqrt_mul
added theorem real.sqrt_mul_self
added theorem real.sqrt_nonneg
added theorem real.sqrt_one
added theorem real.sqrt_pos
added theorem real.sqrt_sqr
added theorem real.sqrt_sqr_eq_abs
added theorem real.sqrt_zero