Slice

📁 Source: PhysLean/SpaceAndTime/Space/Slice.lean

Statistics

Metric	Count
Definitions slice	1
Theorems abs_right_le_norm_slice_symm, basis_self_eq_slice, basis_succAbove_eq_slice, fderiv_fun_slice_symm_left_apply, fderiv_fun_slice_symm_right_apply, fderiv_slice_symm, fderiv_slice_symm_left_apply, fderiv_slice_symm_right_apply, norm_left_le_norm_slice_symm, norm_slice_symm_eq, slice_symm_apply, slice_symm_apply_self, slice_symm_apply_succAbove, slice_symm_measurableEmbedding	14
Total	15

Space

Definitions

Name	Category	Theorems
slice 📖	CompOp	28 math math: schwartzMap_fderiv_integrable_slice_symm, slice_symm_apply_succAbove, schwartzMap_slice_integral_differentiable, fderiv_slice_symm_right_apply, schwartzMap_slice_integral_iteratedFDeriv_apply, basis_succAbove_eq_slice, basis_self_eq_slice, schwartzMap_slice_bound, schwartzMap_integrable_slice_symm, continuous_schwartzMap_slice_integral, schwartzMap_fderiv_left_integrable_slice_symm, schwartzMap_mul_pow_slice_integral_iteratedFDeriv_norm_le, norm_slice_symm_eq, fderiv_slice_symm, schwartzMap_slice_integral_contDiff, schwartzMap_slice_integral_iteratedFDeriv_norm_le, schwartzMap_slice_integral_hasFDerivAt, slice_symm_apply, schwartzMap_mul_iteratedFDeriv_integrable_slice_symm, norm_left_le_norm_slice_symm, schwartzMap_iteratedFDeriv_norm_slice_symm_integrable, fderiv_slice_symm_left_apply, schwartzMap_slice_integral_iteratedFDeriv, slice_symm_apply_self, abs_right_le_norm_slice_symm, sliceSchwartz_apply, schwartzMap_iteratedFDeriv_slice_symm_integrable, slice_symm_measurableEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_right_le_norm_slice_symm 📖	mathematical	—	Space instNorm instSeminormedAddCommGroup instAddCommMonoid instModuleReal slice	—	norm_slice_symm_eq
basis_self_eq_slice 📖	mathematical	—	Space instNormedAddCommGroup instInnerProductSpaceReal basis instSeminormedAddCommGroup instAddCommMonoid instModuleReal slice instZero	—	eq_of_apply basis_self slice_symm_apply_self basis_apply slice_symm_apply_succAbove zero_apply
basis_succAbove_eq_slice 📖	mathematical	—	Space instNormedAddCommGroup instInnerProductSpaceReal basis instSeminormedAddCommGroup instAddCommMonoid instModuleReal slice	—	eq_of_apply basis_apply slice_symm_apply_self slice_symm_apply_succAbove
fderiv_fun_slice_symm_left_apply 📖	mathematical	Space instAddCommGroup instModuleReal instSeminormedAddCommGroup instAddCommMonoid slice	instZero	—	fderiv_slice_symm_left_apply
fderiv_fun_slice_symm_right_apply 📖	—	Space instAddCommGroup instModuleReal instSeminormedAddCommGroup instAddCommMonoid slice	—	—	fderiv_slice_symm_right_apply
fderiv_slice_symm 📖	mathematical	—	Space instAddCommGroup instAddCommMonoid instModuleReal instSeminormedAddCommGroup slice	—	—
fderiv_slice_symm_left_apply 📖	mathematical	—	Space instSeminormedAddCommGroup instAddCommGroup instModuleReal instAddCommMonoid slice instZero	—	fderiv_slice_symm
fderiv_slice_symm_right_apply 📖	mathematical	—	Space instSeminormedAddCommGroup instAddCommGroup instModuleReal instAddCommMonoid slice	—	fderiv_slice_symm
norm_left_le_norm_slice_symm 📖	mathematical	—	Space instNorm instSeminormedAddCommGroup instAddCommMonoid instModuleReal slice	—	norm_slice_symm_eq
norm_slice_symm_eq 📖	mathematical	—	Space instNorm instSeminormedAddCommGroup instAddCommMonoid instModuleReal slice	—	norm_eq slice_symm_apply_self slice_symm_apply_succAbove
slice_symm_apply 📖	mathematical	—	val Space instSeminormedAddCommGroup instAddCommMonoid instModuleReal slice	—	—
slice_symm_apply_self 📖	mathematical	—	val Space instSeminormedAddCommGroup instAddCommMonoid instModuleReal slice	—	slice_symm_apply
slice_symm_apply_succAbove 📖	mathematical	—	val Space instSeminormedAddCommGroup instAddCommMonoid instModuleReal slice	—	slice_symm_apply
slice_symm_measurableEmbedding 📖	mathematical	—	Space instMeasurableSpace instSeminormedAddCommGroup instAddCommMonoid instModuleReal slice	—	instBorelSpace instFiniteDimensionalReal eval_continuous

---

← Back to Index