LocalFrame

📁 Source: Mathlib/Geometry/Manifold/VectorBundle/LocalFrame.lean

Statistics

Metric	Count
Definitions IsLocalFrameOn, coeff, fintypeOfFiniteDimensional, fintype_of_finiteDimensional, toBasisAt, basisAt, localFrame	7
Theorems coeff_apply_of_mem, coeff_apply_of_notMem, coeff_apply_zero_at, coeff_congr, coeff_eq_of_eq, coeff_sum_eq, contMDiffAt, contMDiffAt_of_coeff, contMDiffAt_of_coeff_aux, contMDiffOn, contMDiffOn_of_coeff, eq_iff_coeff, eventually_eq_sum_coeff_smul, generating, linearIndependent, mdifferentiableAt_of_coeff, mdifferentiableAt_of_coeff_aux, mdifferentiableOn_of_coeff, mono, toBasisAt_coe, contMDiffOn_localFrame_baseSet, isLocalFrameOn_localFrame_baseSet, localFrame_apply_of_mem_baseSet, localFrame_apply_of_notMem, contMDiffAt_localFrame_of_mem	25
Total	32

IsLocalFrameOn

Definitions

Name	Category	Theorems
coeff 📖	CompOp	8 math math: coeff_apply_of_mem, coeff_congr, eventually_eq_sum_coeff_smul, coeff_apply_of_notMem, coeff_apply_zero_at, eq_iff_coeff, coeff_eq_of_eq, coeff_sum_eq
fintypeOfFiniteDimensional 📖	CompOp	—
fintype_of_finiteDimensional 📖	CompOp	—
toBasisAt 📖	CompOp	2 math math: coeff_apply_of_mem, toBasisAt_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeff_apply_of_mem 📖	mathematical	IsLocalFrameOn Set Set.instMembership	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid AddCommGroup.toAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Pi.module Pi.Function.module NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace LinearMap.instFunLike coeff Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instFunLike LinearEquiv RingHomInvPair.ids Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr toBasisAt	—	RingHomInvPair.ids
coeff_apply_of_notMem 📖	mathematical	IsLocalFrameOn Set Set.instMembership	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid AddCommGroup.toAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Pi.module Pi.Function.module NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace LinearMap.instFunLike coeff MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing	—	—
coeff_apply_zero_at 📖	mathematical	IsLocalFrameOn NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid AddCommGroup.toAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Pi.module Pi.Function.module NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace LinearMap.instFunLike coeff MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing	—	coeff_congr map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
coeff_congr 📖	mathematical	IsLocalFrameOn	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid AddCommGroup.toAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Pi.module Pi.Function.module NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace LinearMap.instFunLike coeff	—	—
coeff_eq_of_eq 📖	mathematical	IsLocalFrameOn	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid AddCommGroup.toAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Pi.module Pi.Function.module NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace LinearMap.instFunLike coeff	—	linearIndependent generating Submodule.mem_top RingHomInvPair.ids
coeff_sum_eq 📖	mathematical	IsLocalFrameOn Set Set.instMembership	Finset.sum AddCommGroup.toAddCommMonoid Finset.univ SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Pi.module Pi.Function.module NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace LinearMap.instFunLike coeff	—	Finset.sum_congr RingHomInvPair.ids toBasisAt_coe Module.Basis.sum_repr
contMDiffAt 📖	mathematical	IsLocalFrameOn IsOpen Set Set.instMembership	ContMDiffAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod modelWithCornersSelf Bundle.TotalSpace FiberBundle.chartedSpace Bundle.TotalSpace.mk'	—	ContMDiffOn.contMDiffAt contMDiffOn IsOpen.mem_nhds
contMDiffAt_of_coeff 📖	mathematical	IsLocalFrameOn ContMDiffAt NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing modelWithCornersSelf chartedSpaceSelf DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid AddCommGroup.toAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Pi.module Pi.Function.module NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing LinearMap.instFunLike coeff Set Filter Filter.instMembership nhds	Prod.normedAddCommGroup Prod.normedSpace NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod Bundle.TotalSpace FiberBundle.chartedSpace Bundle.TotalSpace.mk'	—	mem_of_mem_nhds ContMDiffAt.sum_section ContMDiffAt.smul_section ContMDiffOn.contMDiffAt contMDiffOn ContMDiffAt.congr_of_eventuallyEq Filter.Eventually.mono eventually_eq_sum_coeff_smul
contMDiffAt_of_coeff_aux 📖	mathematical	IsLocalFrameOn ContMDiffAt NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing modelWithCornersSelf chartedSpaceSelf DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid AddCommGroup.toAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Pi.module Pi.Function.module NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing LinearMap.instFunLike coeff IsOpen Set Set.instMembership	Prod.normedAddCommGroup Prod.normedSpace NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod Bundle.TotalSpace FiberBundle.chartedSpace Bundle.TotalSpace.mk'	—	contMDiffAt_of_coeff IsOpen.mem_nhds
contMDiffOn 📖	mathematical	IsLocalFrameOn	ContMDiffOn Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod modelWithCornersSelf Bundle.TotalSpace FiberBundle.chartedSpace Bundle.TotalSpace.mk'	—	—
contMDiffOn_of_coeff 📖	mathematical	IsLocalFrameOn ContMDiffOn NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing modelWithCornersSelf chartedSpaceSelf DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid AddCommGroup.toAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Pi.module Pi.Function.module NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing LinearMap.instFunLike coeff	Prod.normedAddCommGroup Prod.normedSpace NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod Bundle.TotalSpace FiberBundle.chartedSpace Bundle.TotalSpace.mk'	—	Set.eq_empty_or_nonempty ContMDiffOn.smul_section contMDiffOn ContMDiffOn.sum_section ContMDiffOn.congr coeff_sum_eq
eq_iff_coeff 📖	mathematical	IsLocalFrameOn Set Set.instMembership	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid AddCommGroup.toAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Pi.module Pi.Function.module NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace LinearMap.instFunLike coeff	—	coeff_congr coeff_sum_eq Finset.sum_congr
eventually_eq_sum_coeff_smul 📖	mathematical	IsLocalFrameOn Set Filter Filter.instMembership nhds	Filter.Eventually Finset.sum AddCommGroup.toAddCommMonoid Finset.univ SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Pi.module Pi.Function.module NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedField.toNormedSpace LinearMap.instFunLike coeff	—	Filter.eventually_of_mem coeff_sum_eq
generating 📖	mathematical	IsLocalFrameOn Set Set.instMembership	Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Top.top Submodule.instTop Submodule.span Set.range	—	—
linearIndependent 📖	mathematical	IsLocalFrameOn Set Set.instMembership	LinearIndependent DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid	—	—
mdifferentiableAt_of_coeff 📖	mathematical	IsLocalFrameOn WithTop ENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat MDifferentiableAt NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing modelWithCornersSelf chartedSpaceSelf DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Pi.addCommMonoid AddCommGroup.toAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Pi.module Pi.Function.module NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing LinearMap.instFunLike coeff Set Filter Filter.instMembership nhds	Prod.normedAddCommGroup Prod.normedSpace NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod Bundle.TotalSpace FiberBundle.chartedSpace Bundle.TotalSpace.mk'	—	mem_of_mem_nhds MDifferentiableAt.sum_section MDifferentiableAt.smul_section MDifferentiableOn.mdifferentiableAt ContMDiffOn.mdifferentiableOn contMDiffOn one_ne_zero NeZero.charZero_one WithTop.charZero MDifferentiableAt.congr_of_eventuallyEq Filter.Eventually.mono eventually_eq_sum_coeff_smul
mdifferentiableAt_of_coeff_aux 📖	mathematical	IsLocalFrameOn WithTop ENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat MDifferentiableAt NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing modelWithCornersSelf chartedSpaceSelf DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Pi.addCommMonoid AddCommGroup.toAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Pi.module Pi.Function.module NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing LinearMap.instFunLike coeff IsOpen Set Set.instMembership	Prod.normedAddCommGroup Prod.normedSpace NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod Bundle.TotalSpace FiberBundle.chartedSpace Bundle.TotalSpace.mk'	—	mdifferentiableAt_of_coeff IsOpen.mem_nhds
mdifferentiableOn_of_coeff 📖	mathematical	IsLocalFrameOn WithTop ENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat MDifferentiableOn NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing modelWithCornersSelf chartedSpaceSelf DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Pi.addCommMonoid AddCommGroup.toAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Pi.module Pi.Function.module NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing LinearMap.instFunLike coeff	Prod.normedAddCommGroup Prod.normedSpace NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod Bundle.TotalSpace FiberBundle.chartedSpace Bundle.TotalSpace.mk'	—	Set.eq_empty_or_nonempty MDifferentiableOn.smul_section ContMDiffOn.mdifferentiableOn contMDiffOn one_ne_zero NeZero.charZero_one WithTop.charZero MDifferentiableOn.sum_section MDifferentiableOn.congr coeff_sum_eq
mono 📖	—	IsLocalFrameOn Set Set.instHasSubset	—	—	linearIndependent generating ContMDiffOn.mono contMDiffOn
toBasisAt_coe 📖	mathematical	IsLocalFrameOn Set Set.instMembership	DFunLike.coe Module.Basis DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid Module.Basis.instFunLike toBasisAt	—	Module.Basis.mk_apply linearIndependent generating

Trivialization

Definitions

Name	Category	Theorems
basisAt 📖	CompOp	1 math math: localFrame_apply_of_mem_baseSet
localFrame 📖	CompOp	5 math math: localFrame_apply_of_notMem, contMDiffOn_localFrame_baseSet, contMDiffAt_localFrame_of_mem, isLocalFrameOn_localFrame_baseSet, localFrame_apply_of_mem_baseSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contMDiffOn_localFrame_baseSet 📖	mathematical	—	ContMDiffOn Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod modelWithCornersSelf Bundle.TotalSpace FiberBundle.chartedSpace Bundle.TotalSpace.mk' localFrame baseSet Bundle.TotalSpace.proj	—	contMDiffOn_section_baseSet_iff ContMDiffOn.congr contMDiffOn_const localFrame_apply_of_mem_baseSet apply_mk_symm
isLocalFrameOn_localFrame_baseSet 📖	mathematical	—	IsLocalFrameOn localFrame baseSet Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj	—	localFrame_apply_of_mem_baseSet Module.Basis.linearIndependent Eq.ge Module.Basis.span_eq contMDiffOn_localFrame_baseSet
localFrame_apply_of_mem_baseSet 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj	localFrame DFunLike.coe Module.Basis DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid Module.Basis.instFunLike basisAt	—	—
localFrame_apply_of_notMem 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj	localFrame NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—

(root)

Definitions

Name	Category	Theorems
IsLocalFrameOn 📖	CompData	1 math math: Trivialization.isLocalFrameOn_localFrame_baseSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contMDiffAt_localFrame_of_mem 📖	mathematical	Set Set.instMembership Trivialization.baseSet Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj	ContMDiffAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField ModelProd instTopologicalSpaceModelProd ModelWithCorners.prod modelWithCornersSelf FiberBundle.chartedSpace Bundle.TotalSpace.mk' Trivialization.localFrame	—	IsLocalFrameOn.contMDiffAt Trivialization.isLocalFrameOn_localFrame_baseSet Trivialization.open_baseSet

---

← Back to Index