Commit 2023-01-17 09:04 f20a2b3a

View on Github →

feat: port Data.Real.Basic (#1514)

Estimated changes

added theorem Real.add_neg_lt_supₛ
added theorem Real.cauSeq_converges
added theorem Real.cauchy_add
added theorem Real.cauchy_intCast
added theorem Real.cauchy_inv
added theorem Real.cauchy_mul
added theorem Real.cauchy_natCast
added theorem Real.cauchy_neg
added theorem Real.cauchy_one
added theorem Real.cauchy_ratCast
added theorem Real.cauchy_sub
added theorem Real.cauchy_zero
added theorem Real.cinfᵢ_empty
added theorem Real.csupᵢ_empty
added def Real.equivCauchy
added theorem Real.exists_floor
added theorem Real.exists_isLUB
added theorem Real.ext_cauchy
added theorem Real.ext_cauchy_iff
added theorem Real.infₛ_def
added theorem Real.infₛ_empty
added theorem Real.infₛ_le_iff
added theorem Real.infₛ_le_supₛ
added theorem Real.infₛ_nonneg
added theorem Real.infₛ_nonpos
added theorem Real.isCauSeq_iff_lift
added theorem Real.le_supₛ_iff
added theorem Real.lt_cauchy
added theorem Real.lt_infₛ_add_pos
added def Real.mk
added theorem Real.mk_add
added theorem Real.mk_eq
added theorem Real.mk_inf
added theorem Real.mk_le
added theorem Real.mk_lt
added theorem Real.mk_mul
added theorem Real.mk_neg
added theorem Real.mk_one
added theorem Real.mk_pos
added theorem Real.mk_sup
added theorem Real.mk_zero
added theorem Real.ofCauchy_add
added theorem Real.ofCauchy_inf
added theorem Real.ofCauchy_intCast
added theorem Real.ofCauchy_inv
added theorem Real.ofCauchy_mul
added theorem Real.ofCauchy_natCast
added theorem Real.ofCauchy_neg
added theorem Real.ofCauchy_one
added theorem Real.ofCauchy_ratCast
added theorem Real.ofCauchy_sub
added theorem Real.ofCauchy_sup
added theorem Real.ofCauchy_zero
added theorem Real.of_near
added theorem Real.ratCast_lt
added theorem Real.supₛ_def
added theorem Real.supₛ_empty
added theorem Real.supₛ_nonneg
added theorem Real.supₛ_nonpos
added theorem Real.supₛ_univ
added structure Real