Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-08-28 09:17 79dccba9

View on Github →

refactor: change field notation from k to \bbk (#1363)

refactor: change field notation from k to \bbK
change \bbK to \bbk

Estimated changes

Modified src/analysis/calculus/deriv.lean

modified theorem differentiable.comp

modified theorem differentiable.continuous

modified theorem differentiable.differentiable_on

modified theorem differentiable.mul

modified theorem differentiable.neg

modified theorem differentiable.prod

modified theorem differentiable.smul'

modified theorem differentiable.smul

modified theorem differentiable_at.congr_of_mem_nhds

modified theorem differentiable_at.continuous_at

modified theorem differentiable_at.has_fderiv_at

modified theorem differentiable_at.mul

modified theorem differentiable_at.neg

modified theorem differentiable_at.prod

modified theorem differentiable_at.smul'

modified theorem differentiable_at.smul

modified theorem differentiable_at_const

modified theorem differentiable_at_id

modified theorem differentiable_const

modified theorem differentiable_id

modified theorem differentiable_on.congr_mono

modified theorem differentiable_on.continuous_on

modified theorem differentiable_on.mono

modified theorem differentiable_on.mul

modified theorem differentiable_on.neg

modified theorem differentiable_on.prod

modified theorem differentiable_on.smul'

modified theorem differentiable_on.smul

modified theorem differentiable_on_const

modified theorem differentiable_on_id

modified theorem differentiable_within_at.congr_mono

modified theorem differentiable_within_at.continuous_within_at

modified theorem differentiable_within_at.fderiv_within_congr_mono

modified theorem differentiable_within_at.has_fderiv_within_at

modified theorem differentiable_within_at.mono

modified theorem differentiable_within_at.neg

modified theorem differentiable_within_at.smul

modified theorem differentiable_within_at_const

modified theorem differentiable_within_at_id

modified def fderiv

modified theorem fderiv_const

modified theorem fderiv_id

modified theorem fderiv_mul

modified theorem fderiv_neg

modified theorem fderiv_smul'

modified theorem fderiv_smul

modified def fderiv_within

modified theorem fderiv_within_add

modified theorem fderiv_within_congr

modified theorem fderiv_within_congr_of_mem_nhds_within

modified theorem fderiv_within_const

modified theorem fderiv_within_id

modified theorem fderiv_within_inter

modified theorem fderiv_within_mul

modified theorem fderiv_within_neg

modified theorem fderiv_within_smul'

modified theorem fderiv_within_smul

modified theorem fderiv_within_sub

modified theorem fderiv_within_subset

modified theorem fderiv_within_univ

modified theorem has_fderiv_at.comp

modified theorem has_fderiv_at.comp_has_fderiv_within_at

modified theorem has_fderiv_at.differentiable_at

modified theorem has_fderiv_at.fderiv

modified theorem has_fderiv_at.smul

modified def has_fderiv_at

modified theorem has_fderiv_at_filter.comp

modified theorem has_fderiv_at_filter.smul

modified def has_fderiv_at_filter

modified theorem has_fderiv_at_id

modified theorem has_fderiv_within_at.comp

modified theorem has_fderiv_within_at.smul

modified def has_fderiv_within_at

modified theorem is_bounded_bilinear_map.continuous

modified theorem is_bounded_bilinear_map.differentiable

modified theorem is_bounded_bilinear_map.differentiable_at

modified theorem is_bounded_bilinear_map.differentiable_on

modified theorem is_bounded_bilinear_map.differentiable_within_at

modified theorem is_bounded_bilinear_map.fderiv

modified theorem is_bounded_bilinear_map.fderiv_within

modified theorem is_bounded_bilinear_map.has_fderiv_at

modified theorem is_bounded_bilinear_map.has_fderiv_within_at

modified theorem is_bounded_linear_map.differentiable

modified theorem is_bounded_linear_map.differentiable_at

modified theorem is_bounded_linear_map.differentiable_on

modified theorem is_bounded_linear_map.differentiable_within_at

modified theorem is_bounded_linear_map.fderiv

modified theorem is_bounded_linear_map.fderiv_within

modified theorem is_bounded_linear_map.has_fderiv_at

modified theorem is_bounded_linear_map.has_fderiv_at_filter

modified theorem is_bounded_linear_map.has_fderiv_within_at

modified theorem unique_diff_on.eq

modified theorem unique_diff_within_at.eq

Modified src/analysis/calculus/tangent_cone.lean

modified theorem is_open.unique_diff_on

modified theorem is_open.unique_diff_within_at

modified theorem tangent_cone_at.lim_zero

modified theorem tangent_cone_univ

modified theorem unique_diff_on.prod

modified theorem unique_diff_on_inter

modified theorem unique_diff_on_univ

modified theorem unique_diff_within_at.inter

modified theorem unique_diff_within_at.mono

modified theorem unique_diff_within_at_univ

Modified src/analysis/calculus/times_cont_diff.lean

modified theorem is_bounded_bilinear_map.times_cont_diff

modified theorem is_bounded_linear_map.times_cont_diff

modified def iterated_continuous_linear_map.normed_group_rec

modified def iterated_continuous_linear_map.normed_space_rec

modified def iterated_continuous_linear_map

modified def iterated_fderiv

modified def iterated_fderiv_within

modified theorem iterated_fderiv_within_congr

modified theorem times_cont_diff.continuous

modified theorem times_cont_diff.continuous_fderiv

modified theorem times_cont_diff.of_le

modified theorem times_cont_diff.of_succ

modified def times_cont_diff

modified theorem times_cont_diff_const

modified theorem times_cont_diff_fst

modified theorem times_cont_diff_id

modified theorem times_cont_diff_on.congr

modified theorem times_cont_diff_on.congr_mono'

modified theorem times_cont_diff_on.congr_mono

modified theorem times_cont_diff_on.continuous_on

modified theorem times_cont_diff_on.mono

modified theorem times_cont_diff_on.of_succ

modified def times_cont_diff_on

modified theorem times_cont_diff_on_rec.differentiable_on

modified theorem times_cont_diff_on_rec.of_succ

modified def times_cont_diff_on_rec

modified theorem times_cont_diff_rec.continuous

modified theorem times_cont_diff_rec.differentiable

modified theorem times_cont_diff_rec.of_succ

modified def times_cont_diff_rec

modified theorem times_cont_diff_snd

modified theorem times_cont_diff_top

Modified src/analysis/normed_space/banach.lean

modified theorem exists_preimage_norm_le

modified theorem linear_equiv.is_bounded_inv

modified theorem open_mapping

Modified src/analysis/normed_space/bounded_linear_maps.lean

modified theorem continuous_linear_map.is_bounded_linear_map

modified theorem continuous_linear_map.is_bounded_linear_map_comp_left

modified theorem continuous_linear_map.is_bounded_linear_map_comp_right

modified def is_bounded_bilinear_map.deriv

modified theorem is_bounded_bilinear_map.is_bounded_linear_map_deriv

modified def is_bounded_bilinear_map.linear_deriv

modified theorem is_bounded_bilinear_map.map_sub_left

modified theorem is_bounded_bilinear_map.map_sub_right

modified theorem is_bounded_bilinear_map_deriv_coe

modified theorem is_bounded_linear_map.add

modified theorem is_bounded_linear_map.continuous

modified theorem is_bounded_linear_map.fst

modified theorem is_bounded_linear_map.id

modified theorem is_bounded_linear_map.is_O_comp

modified theorem is_bounded_linear_map.is_O_id

modified theorem is_bounded_linear_map.is_O_sub

modified theorem is_bounded_linear_map.lim_zero_bounded_linear_map

modified theorem is_bounded_linear_map.neg

modified theorem is_bounded_linear_map.smul

modified theorem is_bounded_linear_map.snd

modified theorem is_bounded_linear_map.sub

modified theorem is_bounded_linear_map.tendsto

modified def is_bounded_linear_map.to_continuous_linear_map

modified def is_bounded_linear_map.to_linear_map

modified theorem is_bounded_linear_map.zero

modified structure is_bounded_linear_map

Modified src/analysis/normed_space/operator_norm.lean

modified theorem continuous_linear_map.bounds_bdd_below

modified theorem continuous_linear_map.bounds_nonempty

modified theorem continuous_linear_map.is_O_comp

modified theorem continuous_linear_map.is_O_sub

modified theorem continuous_linear_map.norm_id

modified theorem continuous_linear_map.norm_zero

modified theorem continuous_linear_map.scalar_prod_space_iso_norm

modified theorem linear_map.continuous_of_bound

modified def linear_map.with_bound

modified theorem linear_map_with_bound_apply

modified theorem linear_map_with_bound_coe