Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-01-17 09:04
f20a2b3a
View on Github →
feat: port Data.Real.Basic (
#1514
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Data/Real/Basic.lean
added
theorem
CauSeq.Completion.ofRat_rat
added
theorem
Real.add_lt_add_iff_left
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ᵢ_const_zero
added
theorem
Real.cinfᵢ_empty
added
theorem
Real.csupᵢ_const_zero
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ᵢ_of_not_bddBelow
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.infₛ_of_not_bddBelow
added
theorem
Real.isCauSeq_iff_lift
added
theorem
Real.le_mk_of_forall_le
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_le_of_forall_le
added
theorem
Real.mk_lt
added
theorem
Real.mk_mul
added
theorem
Real.mk_near_of_forall_near
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
def
Real.ringEquivCauchy
added
theorem
Real.supᵢ_of_not_bddAbove
added
theorem
Real.supₛ_def
added
theorem
Real.supₛ_empty
added
theorem
Real.supₛ_nonneg
added
theorem
Real.supₛ_nonpos
added
theorem
Real.supₛ_of_not_bddAbove
added
theorem
Real.supₛ_univ
added
structure
Real
Created
test/Real.lean
Modified
test/linear_combination.lean
Modified
test/norm_num.lean