ContMDiffMap

📁 Source: Mathlib/Geometry/Manifold/ContMDiffMap.lean

Statistics

Metric	Count
Definitions ContMDiffMap, comp, const, fst, id, instFunLike, instInhabited, prodMk, snd, hasCoeToContMDiffMap, «termC^_⟮_,_;_,_⟯», «termC^_⟮_,_;_⟯»	12
Theorems coeFn_mk, coe_injective, comp_apply, contMDiff, ext, ext_iff, instContinuousMapClass	7
Total	19

ContMDiffMap

Definitions

Name	Category	Theorems
comp 📖	CompOp	10 math math: add_comp, LeftInvariantDerivation.comp_L, fdifferential_apply, smul_comp, L_mul, R_mul, fdifferential_comp, smul_comp', mul_comp, comp_apply
const 📖	CompOp	—
fst 📖	CompOp	—
id 📖	CompOp	—
instFunLike 📖	CompOp	91 math math: coeFnMonoidHom_apply, SmoothBumpCovering.toSmoothPartitionOfUnity_eq_mul_prod, exists_contMDiffMap_zero_one_of_isClosed, coeFnAlgHom_apply, SmoothPartitionOfUnity.contMDiffAt_finsum, SmoothPartitionOfUnity.locallyFinite, exists_smooth_one_nhds_of_subset_interior, SmoothPartitionOfUnity.nonneg, SmoothPartitionOfUnity.locallyFinite', ContMDiffVectorBundle.pullback, Diffeomorph.coe_coe, SmoothPartitionOfUnity.sum_finsupport', coe_nsmul, SmoothBumpCovering.toSmoothPartitionOfUnity_apply, SmoothPartitionOfUnity.contDiffAt_finsum, Metric.exists_smooth_forall_closedBall_subset, coe_sub, SmoothPartitionOfUnity.le_one, Continuous.exists_contMDiff_approx, exists_contMDiffMap_zero_one_nhds_of_isClosed, fdifferential_apply, SmoothBumpCovering.sum_toSmoothPartitionOfUnity_eq, SmoothPartitionOfUnity.sum_eq_one', contMDiff, SmoothPartitionOfUnity.mem_finsupport, smoothRightMul_one, coe_mul, coe_add, exists_contMDiffOn_forall_mem_convex_of_local, SmoothBumpCovering.embeddingPiTangent_injective_mfderiv, SmoothPartitionOfUnity.coe_finsupport, Emetric.exists_contMDiffMap_forall_closedBall_subset, coe_pow, mdifferentiable', coe_zero, smoothLeftMul_one, Metric.exists_contMDiffMap_forall_closedBall_subset, SmoothPartitionOfUnity.finsum_smul_mem_convex, SmoothPartitionOfUnity.sum_le_one', SmoothBumpCovering.embeddingPiTangent_ker_mfderiv, SmoothPartitionOfUnity.sum_nonneg, fdifferential_comp, SmoothBumpCovering.exists_finset_toSmoothPartitionOfUnity_eventuallyEq, mdifferentiable, coe_smul, SmoothPartitionOfUnity.sum_eq_one, coe_neg, SmoothBumpCovering.embeddingPiTangent_injOn, Continuous.exists_contMDiff_approx_and_eqOn, coeFnAddMonoidHom_apply, L_apply, exists_contMDiffMap_forall_mem_convex_of_local, coe_div, SmoothBumpCovering.comp_embeddingPiTangent_mfderiv, SmoothPartitionOfUnity.exists_pos_of_mem, exists_smooth_zero_one_of_isClosed, SmoothBumpCovering.embeddingPiTangent_injective, SmoothPartitionOfUnity.sum_finsupport_smul_eq_finsum, R_apply, SmoothPartitionOfUnity.contMDiff_finsum_smul, SmoothPartitionOfUnity.sum_finsupport, exists_smooth_forall_mem_convex_of_local_const, SmoothBumpCovering.support_toSmoothPartitionOfUnity_subset, mdifferentiableAt, SmoothPartitionOfUnity.finite_tsupport, BumpCovering.coe_toSmoothPartitionOfUnity, SmoothPartitionOfUnity.mem_fintsupport_iff, Emetric.exists_smooth_forall_closedBall_subset, exists_smooth_forall_mem_convex_of_local, coe_one, coeFnRingHom_apply, SmoothPartitionOfUnity.toPartitionOfUnity_toFun, SmoothPartitionOfUnity.contMDiff_smul, coeFn_mk, coe_inv, exists_smooth_zero_one_nhds_of_isClosed, ext_iff, SmoothBumpCovering.embeddingPiTangent_coe, SmoothPartitionOfUnity.nonneg', SmoothPartitionOfUnity.IsSubordinate.contMDiff_finsum_smul, exists_contMDiffMap_one_nhds_of_subset_interior, SmoothPartitionOfUnity.sum_le_one, exists_contMDiffMap_forall_mem_convex_of_local_const, instContinuousMapClass, Derivation.evalAt_apply, SmoothBumpCovering.toSmoothPartitionOfUnity_zero_of_zero, SmoothPartitionOfUnity.contMDiff_sum, Metric.exists_contMDiffMap_forall_closedEBall_subset, coeFnLinearMap_apply, comp_apply, LeftInvariantDerivation.evalAt_apply
instInhabited 📖	CompOp	—
prodMk 📖	CompOp	—
snd 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeFn_mk 📖	mathematical	ContMDiff	DFunLike.coe ContMDiffMap instFunLike	—	—
coe_injective 📖	—	DFunLike.coe ContMDiffMap instFunLike	—	—	DFunLike.ext'
comp_apply 📖	mathematical	—	DFunLike.coe ContMDiffMap instFunLike comp	—	—
contMDiff 📖	mathematical	—	ContMDiff DFunLike.coe ContMDiffMap instFunLike	—	Subtype.prop
ext 📖	—	DFunLike.coe ContMDiffMap instFunLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe ContMDiffMap instFunLike	—	ext
instContinuousMapClass 📖	mathematical	—	ContinuousMapClass ContMDiffMap instFunLike	—	ContMDiff.continuous contMDiff

ContinuousLinearMap

Definitions

Name	Category	Theorems
hasCoeToContMDiffMap 📖	CompOp	—

Manifold

Definitions

Name	Category	Theorems
«termC^_⟮_,_;_,_⟯» 📖	CompOp	—
«termC^_⟮_,_;_⟯» 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
ContMDiffMap 📖	CompOp	125 math math: ContMDiffMap.coeFnMonoidHom_apply, SmoothBumpCovering.toSmoothPartitionOfUnity_eq_mul_prod, LeftInvariantDerivation.lift_zero, exists_contMDiffMap_zero_one_of_isClosed, LeftInvariantDerivation.leibniz, ContMDiffMap.coeFnAlgHom_apply, SmoothPartitionOfUnity.contMDiffAt_finsum, LeftInvariantDerivation.coe_derivation, SmoothPartitionOfUnity.locallyFinite, exists_smooth_one_nhds_of_subset_interior, SmoothPartitionOfUnity.nonneg, LeftInvariantDerivation.left_invariant', ContMDiffMap.add_comp, SmoothPartitionOfUnity.locallyFinite', ContMDiffVectorBundle.pullback, Diffeomorph.coe_coe, LeftInvariantDerivation.lift_add, LeftInvariantDerivation.lift_smul, SmoothPartitionOfUnity.sum_finsupport', LeftInvariantDerivation.comp_L, ContMDiffMap.coe_nsmul, SmoothBumpCovering.toSmoothPartitionOfUnity_apply, SmoothPartitionOfUnity.contDiffAt_finsum, Metric.exists_smooth_forall_closedBall_subset, LeftInvariantDerivation.evalAt_coe, ContMDiffMap.coe_sub, SmoothPartitionOfUnity.le_one, Continuous.exists_contMDiff_approx, exists_contMDiffMap_zero_one_nhds_of_isClosed, LeftInvariantDerivation.map_zero, fdifferential_apply, ContMDiffMap.smul_comp, SmoothBumpCovering.sum_toSmoothPartitionOfUnity_eq, LeftInvariantDerivation.coe_sub, LeftInvariantDerivation.left_invariant'', SmoothPartitionOfUnity.sum_eq_one', ContMDiffMap.contMDiff, SmoothPartitionOfUnity.mem_finsupport, smoothRightMul_one, ContMDiffMap.coe_mul, ContMDiffMap.coe_add, exists_contMDiffOn_forall_mem_convex_of_local, SmoothBumpCovering.embeddingPiTangent_injective_mfderiv, SmoothPartitionOfUnity.coe_finsupport, Emetric.exists_contMDiffMap_forall_closedBall_subset, ContMDiffMap.coe_pow, ContMDiffMap.mdifferentiable', ContMDiffMap.coe_zero, smoothLeftMul_one, Metric.exists_contMDiffMap_forall_closedBall_subset, LeftInvariantDerivation.map_add, smoothSheaf.obj_eq, SmoothPartitionOfUnity.finsum_smul_mem_convex, LeftInvariantDerivation.coe_add, SmoothPartitionOfUnity.sum_le_one', SmoothBumpCovering.embeddingPiTangent_ker_mfderiv, SmoothPartitionOfUnity.sum_nonneg, fdifferential_comp, LeftInvariantDerivation.coe_injective, SmoothBumpCovering.exists_finset_toSmoothPartitionOfUnity_eventuallyEq, LeftInvariantDerivation.coe_neg, ContMDiffMap.mdifferentiable, ContMDiffMap.coe_smul, LeftInvariantDerivation.map_smul, SmoothPartitionOfUnity.sum_eq_one, ContMDiffMap.coe_neg, SmoothBumpCovering.embeddingPiTangent_injOn, PointedContMDiffMap.instIsScalarTowerSomeENatTopContMDiffMapModelWithCornersSelf, LeftInvariantDerivation.coe_smul, Continuous.exists_contMDiff_approx_and_eqOn, ContMDiffMap.coeFnAddMonoidHom_apply, L_apply, exists_contMDiffMap_forall_mem_convex_of_local, ContMDiffMap.coe_div, SmoothBumpCovering.comp_embeddingPiTangent_mfderiv, SmoothPartitionOfUnity.exists_pos_of_mem, exists_smooth_zero_one_of_isClosed, SmoothBumpCovering.embeddingPiTangent_injective, LeftInvariantDerivation.map_sub, SmoothPartitionOfUnity.sum_finsupport_smul_eq_finsum, LeftInvariantDerivation.map_neg, R_apply, SmoothPartitionOfUnity.contMDiff_finsum_smul, SmoothPartitionOfUnity.sum_finsupport, exists_smooth_forall_mem_convex_of_local_const, SmoothBumpCovering.support_toSmoothPartitionOfUnity_subset, ContMDiffMap.mdifferentiableAt, SmoothPartitionOfUnity.finite_tsupport, ContMDiffMap.smul_comp', LeftInvariantDerivation.coe_zero, LeftInvariantDerivation.toDerivation_injective, BumpCovering.coe_toSmoothPartitionOfUnity, SmoothPartitionOfUnity.mem_fintsupport_iff, Emetric.exists_smooth_forall_closedBall_subset, ContMDiffMap.mul_comp, exists_smooth_forall_mem_convex_of_local, ContMDiffMap.coe_one, ContMDiffMap.coeFnRingHom_apply, LeftInvariantDerivation.commutator_apply, LeftInvariantDerivation.commutator_coe_derivation, SmoothPartitionOfUnity.toPartitionOfUnity_toFun, SmoothPartitionOfUnity.contMDiff_smul, ContMDiffMap.coeFn_mk, LeftInvariantDerivation.ext_iff, ContMDiffMap.coe_inv, exists_smooth_zero_one_nhds_of_isClosed, ContMDiffMap.ext_iff, LeftInvariantDerivation.toFun_eq_coe, SmoothBumpCovering.embeddingPiTangent_coe, SmoothPartitionOfUnity.nonneg', SmoothPartitionOfUnity.IsSubordinate.contMDiff_finsum_smul, exists_contMDiffMap_one_nhds_of_subset_interior, SmoothPartitionOfUnity.sum_le_one, exists_contMDiffMap_forall_mem_convex_of_local_const, smooth_functions_tower, ContMDiffMap.instContinuousMapClass, LeftInvariantDerivation.instLinearMapClassContMDiffMapModelWithCornersSelfSomeENatTop, LeftInvariantDerivation.coeFnAddMonoidHom_apply, Derivation.evalAt_apply, SmoothBumpCovering.toSmoothPartitionOfUnity_zero_of_zero, SmoothPartitionOfUnity.contMDiff_sum, Metric.exists_contMDiffMap_forall_closedEBall_subset, ContMDiffMap.coeFnLinearMap_apply, ContMDiffMap.comp_apply, LeftInvariantDerivation.evalAt_apply

---

← Back to Index