Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-24 12:36 839b92fe

View on Github →

feat(data/nat/enat): new file (#16217) Define enat := with_top nat, use notation.

Estimated changes

modified def cont_diff_at
modified theorem cont_diff_clm_apply
modified theorem cont_diff_on_clm_apply
modified def cont_diff_within_at
modified structure has_ftaylor_series_up_to
modified structure has_ftaylor_series_up_to_on
modified theorem analytic_on.cont_diff_on
modified theorem cont_diff.real_of_complex
modified theorem cont_diff_at_euclidean
modified theorem cont_diff_euclidean
modified theorem cont_diff_on_euclidean
modified theorem real.cont_diff_arsinh
modified theorem complex.cont_diff_at_log
modified theorem real.cont_diff_at_log
modified theorem real.cont_diff_on_log
modified theorem real.cont_diff_at_sqrt
modified theorem real.cont_diff_arctan
modified theorem complex.cont_diff_at_tan
modified theorem real.cont_diff_at_arccos
modified theorem real.cont_diff_at_arcsin
modified theorem real.cont_diff_on_arccos
modified theorem real.cont_diff_on_arcsin
deleted theorem with_top.add_one_le_of_lt
deleted theorem with_top.nat_induction
deleted theorem with_top.one_le_iff_pos
added theorem enat.add_one_le_iff
added theorem enat.add_one_le_of_lt
added theorem enat.coe_add
added theorem enat.coe_mul
added theorem enat.coe_one
added theorem enat.coe_sub
added theorem enat.coe_zero
added theorem enat.le_of_lt_add_one
added theorem enat.nat_induction
added theorem enat.one_le_iff_pos
added theorem enat.succ_def
added def enat.to_nat
added def enat
modified def part_enat.to_with_top
modified def cont_mdiff
modified def cont_mdiff_at
modified theorem cont_mdiff_at_iff
modified def cont_mdiff_on
modified def cont_mdiff_within_at