VectorField

📁 Source: Mathlib/Analysis/Calculus/VectorField.lean

Statistics

Metric	Count
Definitions lieBracket, lieBracketWithin, pullback, pullbackWithin	4
Theorems lieBracket_vectorField, lieBracket_vectorField, lieBracketWithin_vectorField, lieBracketWithin_vectorField, lieBracketWithin_congr_mono, lieBracketWithin_vectorField, lieBracketWithin_vectorField', lieBracketWithin_vectorField_eq, lieBracketWithin_vectorField_eq_nhds, lieBracketWithin_vectorField_eq_of_insert, lieBracketWithin_vectorField_eq_of_mem, lieBracket_vectorField, lieBracket_vectorField_eq, pullbackWithin, fderivWithin_apply_lieBracket, fderivWithin_apply_lieBracket_of_isSymmSndFDerivWithinAt, fderivWithin_pullbackWithin, fderiv_apply_lieBracket, fderiv_apply_lieBracket_of_isSymmSndFDerivAt, fderiv_pullback, leibniz_identity_lieBracket, leibniz_identity_lieBracketWithin, leibniz_identity_lieBracketWithin_of_isSymmSndFDerivWithinAt, lieBracketWithin_add_left, lieBracketWithin_add_right, lieBracketWithin_congr, lieBracketWithin_congr', lieBracketWithin_congr_set, lieBracketWithin_congr_set', lieBracketWithin_const_smul_left, lieBracketWithin_const_smul_right, lieBracketWithin_eq, lieBracketWithin_eq_lieBracket, lieBracketWithin_eq_zero_of_eq_zero, lieBracketWithin_eventually_congr_set, lieBracketWithin_eventually_congr_set', lieBracketWithin_inter, lieBracketWithin_of_isOpen, lieBracketWithin_of_mem_nhds, lieBracketWithin_of_mem_nhdsWithin, lieBracketWithin_self, lieBracketWithin_smul_left, lieBracketWithin_smul_right, lieBracketWithin_subset, lieBracketWithin_swap, lieBracketWithin_univ, lieBracketWithin_zero_left, lieBracketWithin_zero_right, lieBracket_add_left, lieBracket_add_right, lieBracket_const_smul_left, lieBracket_const_smul_right, lieBracket_eq, lieBracket_eq_zero_of_eq_zero, lieBracket_fmul_left, lieBracket_self, lieBracket_smul_left, lieBracket_smul_right, lieBracket_swap, lieBracket_zero_left, lieBracket_zero_right, pullbackWithin_eq, pullbackWithin_eq_of_fderivWithin_eq, pullbackWithin_eq_of_not_isInvertible, pullbackWithin_lieBracketWithin, pullbackWithin_lieBracketWithin_of_isSymmSndFDerivWithinAt, pullbackWithin_lieBracketWithin_of_isSymmSndFDerivWithinAt_of_eventuallyEq, pullbackWithin_univ, pullback_eq_of_fderiv_eq, pullback_eq_of_not_isInvertible, pullback_lieBracket, pullback_lieBracket_of_isSymmSndFDerivAt, exists_continuousLinearEquiv_fderivWithin_symm_eq, exists_continuousLinearEquiv_fderiv_symm_eq	74
Total	78

ContDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lieBracket_vectorField 📖	mathematical	ContDiff WithTop ENat Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat WithTop.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	VectorField.lieBracket	—	contDiff_iff_contDiffAt ContDiffAt.lieBracket_vectorField contDiffAt

ContDiffAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lieBracket_vectorField 📖	mathematical	ContDiffAt WithTop ENat Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat WithTop.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	VectorField.lieBracket	—	contDiffWithinAt_univ ContDiffWithinAt.lieBracketWithin_vectorField uniqueDiffOn_univ PerfectSpace.not_isolated instPerfectSpace IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Set.mem_univ

ContDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lieBracketWithin_vectorField 📖	mathematical	ContDiffOn UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace WithTop ENat Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat WithTop.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	VectorField.lieBracketWithin	—	ContDiffWithinAt.lieBracketWithin_vectorField

ContDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lieBracketWithin_vectorField 📖	mathematical	ContDiffWithinAt UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace WithTop ENat Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat WithTop.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Set Set.instMembership	VectorField.lieBracketWithin	—	sub clm_apply fderivWithin_right of_le le_trans le_self_add WithTop.canonicallyOrderedAdd

DifferentiableWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lieBracketWithin_congr_mono 📖	mathematical	DifferentiableWithinAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set.EqOn UniqueDiffWithinAt DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Set Set.instHasSubset	VectorField.lieBracketWithin	—	fderivWithin_congr_mono IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace

Filter.EventuallyEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lieBracketWithin_vectorField 📖	mathematical	Filter.EventuallyEq nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	VectorField.lieBracketWithin	—	lieBracketWithin_vectorField' Set.Subset.rfl
lieBracketWithin_vectorField' 📖	mathematical	Filter.EventuallyEq nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set Set.instHasSubset	VectorField.lieBracketWithin	—	Filter.mp_mem fderivWithin' Filter.univ_mem'
lieBracketWithin_vectorField_eq 📖	mathematical	Filter.EventuallyEq nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	VectorField.lieBracketWithin	—	fderivWithin_eq
lieBracketWithin_vectorField_eq_nhds 📖	mathematical	Filter.EventuallyEq nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	VectorField.lieBracketWithin	—	lieBracketWithin_vectorField_eq filter_mono nhdsWithin_le_nhds Filter.Eventually.self_of_nhds
lieBracketWithin_vectorField_eq_of_insert 📖	mathematical	Filter.EventuallyEq nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set Set.instInsert	VectorField.lieBracketWithin	—	mem_of_mem_nhdsWithin Set.mem_insert lieBracketWithin_vectorField' Set.subset_insert
lieBracketWithin_vectorField_eq_of_mem 📖	mathematical	Filter.EventuallyEq nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set Set.instMembership	VectorField.lieBracketWithin	—	lieBracketWithin_vectorField_eq mem_of_mem_nhdsWithin
lieBracket_vectorField 📖	mathematical	Filter.EventuallyEq nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	VectorField.lieBracket	—	Filter.mp_mem eventuallyEq_nhds Filter.univ_mem' lieBracket_vectorField_eq
lieBracket_vectorField_eq 📖	mathematical	Filter.EventuallyEq nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	VectorField.lieBracket	—	VectorField.lieBracketWithin_univ lieBracketWithin_vectorField_eq_nhds

VectorField

Definitions

Name	Category	Theorems
lieBracket 📖	CompOp	27 math math: fderiv_apply_lieBracket, fderiv_apply_lieBracket_of_isSymmSndFDerivAt, lieBracketWithin_eq_lieBracket, lieBracket_swap, lieBracketWithin_of_mem_nhds, extDeriv_apply_vectorField, lieBracket_const_smul_left, Filter.EventuallyEq.lieBracket_vectorField, lieBracketWithin_univ, lieBracket_fmul_left, lieBracket_eq, lieBracket_add_left, lieBracket_zero_right, pullback_lieBracket_of_isSymmSndFDerivAt, lieBracket_self, lieBracket_const_smul_right, ContDiffAt.lieBracket_vectorField, lieBracket_smul_left, ContDiff.lieBracket_vectorField, Filter.EventuallyEq.lieBracket_vectorField_eq, lieBracket_add_right, leibniz_identity_lieBracket, pullback_lieBracket, lieBracket_smul_right, lieBracket_zero_left, lieBracketWithin_of_isOpen, lieBracket_eq_zero_of_eq_zero
lieBracketWithin 📖	CompOp	45 math math: lieBracketWithin_zero_left, ContDiffOn.lieBracketWithin_vectorField, lieBracketWithin_of_mem_nhdsWithin, lieBracketWithin_eq_lieBracket, lieBracketWithin_zero_right, pullbackWithin_lieBracketWithin_of_isSymmSndFDerivWithinAt, lieBracketWithin_of_mem_nhds, lieBracketWithin_self, lieBracketWithin_subset, DifferentiableWithinAt.lieBracketWithin_congr_mono, lieBracketWithin_univ, ContDiffWithinAt.lieBracketWithin_vectorField, lieBracketWithin_eventually_congr_set', lieBracketWithin_smul_left, lieBracketWithin_inter, mlieBracketWithin_def, fderivWithin_apply_lieBracket_of_isSymmSndFDerivWithinAt, lieBracketWithin_congr_set', pullbackWithin_lieBracketWithin, extDerivWithin_apply_vectorField, Filter.EventuallyEq.lieBracketWithin_vectorField, leibniz_identity_lieBracketWithin_of_isSymmSndFDerivWithinAt, lieBracketWithin_eq_zero_of_eq_zero, lieBracketWithin_add_left, lieBracketWithin_smul_right, lieBracketWithin_congr', lieBracketWithin_congr, lieBracketWithin_swap, lieBracketWithin_congr_set, lieBracketWithin_eq, fderivWithin_apply_lieBracket, lieBracketWithin_const_smul_right, Filter.EventuallyEq.lieBracketWithin_vectorField_eq, mlieBracketWithin_apply, mlieBracketWithin_eq_lieBracketWithin, Filter.EventuallyEq.lieBracketWithin_vectorField_eq_nhds, lieBracketWithin_add_right, Filter.EventuallyEq.lieBracketWithin_vectorField_eq_of_insert, lieBracketWithin_of_isOpen, Filter.EventuallyEq.lieBracketWithin_vectorField_eq_of_mem, lieBracketWithin_eventually_congr_set, leibniz_identity_lieBracketWithin, Filter.EventuallyEq.lieBracketWithin_vectorField', lieBracketWithin_const_smul_left, pullbackWithin_lieBracketWithin_of_isSymmSndFDerivWithinAt_of_eventuallyEq
pullback 📖	CompOp	7 math math: mpullback_eq_pullback, fderiv_pullback, pullback_lieBracket_of_isSymmSndFDerivAt, pullbackWithin_univ, pullback_eq_of_fderiv_eq, pullback_eq_of_not_isInvertible, pullback_lieBracket
pullbackWithin 📖	CompOp	10 math math: pullbackWithin_eq_of_not_isInvertible, pullbackWithin_lieBracketWithin_of_isSymmSndFDerivWithinAt, pullbackWithin_eq_of_fderivWithin_eq, fderivWithin_pullbackWithin, DifferentiableWithinAt.pullbackWithin, pullbackWithin_lieBracketWithin, pullbackWithin_univ, pullbackWithin_eq, mpullbackWithin_eq_pullbackWithin, pullbackWithin_lieBracketWithin_of_isSymmSndFDerivWithinAt_of_eventuallyEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fderivWithin_apply_lieBracket 📖	mathematical	ContDiffWithinAt WithTop ENat Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat minSmoothness instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Nat.instAtLeastTwoHAddOfNat UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set Set.instMembership closure interior DifferentiableWithinAt	DFunLike.coe ContinuousLinearMap RingHom.id AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike fderivWithin lieBracketWithin SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	Nat.instAtLeastTwoHAddOfNat fderivWithin_apply_lieBracket_of_isSymmSndFDerivWithinAt ContDiffWithinAt.of_le LE.le.trans le_minSmoothness ContDiffWithinAt.isSymmSndFDerivWithinAt
fderivWithin_apply_lieBracket_of_isSymmSndFDerivWithinAt 📖	mathematical	ContDiffWithinAt WithTop ENat instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Nat.instAtLeastTwoHAddOfNat IsSymmSndFDerivWithinAt UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set Set.instMembership DifferentiableWithinAt	DFunLike.coe ContinuousLinearMap RingHom.id AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike fderivWithin lieBracketWithin SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	Nat.instAtLeastTwoHAddOfNat SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul ContDiffWithinAt.differentiableWithinAt RingHomIsometric.ids ContDiffWithinAt.fderivWithin_right one_ne_zero NeZero.charZero_one WithTop.charZero IsTopologicalAddGroup.toContinuousAdd RingHomCompTriple.ids fderivWithin_clm_apply map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass add_sub_add_right_eq_sub
fderivWithin_pullbackWithin 📖	mathematical	ContinuousLinearMap.IsInvertible UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule fderivWithin	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.funLike pullbackWithin	—	RingHomInvPair.ids pullbackWithin_eq_of_fderivWithin_eq ContinuousLinearEquiv.apply_symm_apply
fderiv_apply_lieBracket 📖	mathematical	ContDiffAt WithTop ENat Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat minSmoothness instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Nat.instAtLeastTwoHAddOfNat DifferentiableAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike fderiv lieBracket SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	Nat.instAtLeastTwoHAddOfNat fderiv_apply_lieBracket_of_isSymmSndFDerivAt ContDiffAt.of_le LE.le.trans le_minSmoothness ContDiffAt.isSymmSndFDerivAt
fderiv_apply_lieBracket_of_isSymmSndFDerivAt 📖	mathematical	ContDiffAt WithTop ENat instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Nat.instAtLeastTwoHAddOfNat IsSymmSndFDerivAt DifferentiableAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike fderiv lieBracket SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	Nat.instAtLeastTwoHAddOfNat fderivWithin_apply_lieBracket_of_isSymmSndFDerivWithinAt PerfectSpace.not_isolated instPerfectSpace IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul
fderiv_pullback 📖	mathematical	ContinuousLinearMap.IsInvertible UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule fderiv	DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.funLike pullback	—	RingHomInvPair.ids pullback_eq_of_fderiv_eq ContinuousLinearEquiv.apply_symm_apply
leibniz_identity_lieBracket 📖	mathematical	WithTop ENat Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat minSmoothness instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Nat.instAtLeastTwoHAddOfNat ContDiffAt	lieBracket AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	Nat.instAtLeastTwoHAddOfNat leibniz_identity_lieBracketWithin uniqueDiffOn_univ PerfectSpace.not_isolated instPerfectSpace IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul interior_univ IsClosed.closure_eq Set.mem_univ
leibniz_identity_lieBracketWithin 📖	mathematical	WithTop ENat Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat minSmoothness instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Nat.instAtLeastTwoHAddOfNat UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set Set.instMembership closure interior ContDiffWithinAt	lieBracketWithin AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	Nat.instAtLeastTwoHAddOfNat leibniz_identity_lieBracketWithin_of_isSymmSndFDerivWithinAt ContDiffWithinAt.of_le LE.le.trans le_minSmoothness ContDiffWithinAt.isSymmSndFDerivWithinAt
leibniz_identity_lieBracketWithin_of_isSymmSndFDerivWithinAt 📖	mathematical	UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set Set.instMembership ContDiffWithinAt WithTop ENat instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Nat.instAtLeastTwoHAddOfNat IsSymmSndFDerivWithinAt	lieBracketWithin AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	Nat.instAtLeastTwoHAddOfNat map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass ContDiffWithinAt.fderivWithin_right_apply ContDiffWithinAt.of_le one_le_two WithTop.zeroLEOneClass IsOrderedRing.toZeroLEOneClass WithTop.addLeftMono IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid le_rfl ContDiffWithinAt.differentiableWithinAt one_ne_zero NeZero.charZero_one WithTop.charZero IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup RingHomCompTriple.ids smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomIsometric.ids fderivWithin_clm_apply ContDiffWithinAt.fderivWithin_right two_ne_zero CharZero.NeZero.two fderivWithin_fun_sub IsSymmSndFDerivWithinAt.eq Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Abel.const_add_termg add_zero Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Abel.zero_termg
lieBracketWithin_add_left 📖	mathematical	DifferentiableWithinAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace UniqueDiffWithinAt DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField	lieBracketWithin Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	map_add SemilinearMapClass.toAddHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup fderivWithin_add ContinuousLinearMap.add_apply Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.const_add_termg
lieBracketWithin_add_right 📖	mathematical	DifferentiableWithinAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace UniqueDiffWithinAt DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField	lieBracketWithin Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	map_add SemilinearMapClass.toAddHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup fderivWithin_add ContinuousLinearMap.add_apply Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.const_add_termg
lieBracketWithin_congr 📖	mathematical	Set.EqOn	lieBracketWithin	—	Filter.EventuallyEq.lieBracketWithin_vectorField_eq Filter.EventuallyEq.filter_mono Set.EqOn.eventuallyEq inf_le_right
lieBracketWithin_congr' 📖	mathematical	Set.EqOn Set Set.instMembership	lieBracketWithin	—	lieBracketWithin_congr
lieBracketWithin_congr_set 📖	mathematical	Filter.EventuallyEq nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	lieBracketWithin	—	lieBracketWithin_congr_set' Filter.EventuallyEq.filter_mono inf_le_left
lieBracketWithin_congr_set' 📖	mathematical	Filter.EventuallyEq nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Compl.compl Set Set.instCompl Set.instSingletonSet	lieBracketWithin	—	fderivWithin_congr_set' T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
lieBracketWithin_const_smul_left 📖	mathematical	DifferentiableWithinAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace UniqueDiffWithinAt DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField	lieBracketWithin Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid	—	map_smul SemilinearMapClass.toMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul fderivWithin_const_smul smul_sub
lieBracketWithin_const_smul_right 📖	mathematical	DifferentiableWithinAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace UniqueDiffWithinAt DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField	lieBracketWithin Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid	—	smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul fderivWithin_const_smul map_smul SemilinearMapClass.toMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass smul_sub
lieBracketWithin_eq 📖	mathematical	—	lieBracketWithin SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule ContinuousLinearMap.funLike fderivWithin	—	—
lieBracketWithin_eq_lieBracket 📖	mathematical	UniqueDiffWithinAt DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DifferentiableAt	lieBracketWithin lieBracket	—	fderivWithin_eq_fderiv IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
lieBracketWithin_eq_zero_of_eq_zero 📖	mathematical	NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	lieBracketWithin	—	map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass sub_self
lieBracketWithin_eventually_congr_set 📖	mathematical	Filter.EventuallyEq nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	lieBracketWithin	—	lieBracketWithin_eventually_congr_set' Filter.EventuallyEq.filter_mono inf_le_left
lieBracketWithin_eventually_congr_set' 📖	mathematical	Filter.EventuallyEq nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Compl.compl Set Set.instCompl Set.instSingletonSet	nhds lieBracketWithin	—	Filter.Eventually.mono eventually_nhds_nhdsWithin lieBracketWithin_congr_set'
lieBracketWithin_inter 📖	mathematical	Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	lieBracketWithin Set.instInter	—	fderivWithin_inter
lieBracketWithin_of_isOpen 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set Set.instMembership	lieBracketWithin lieBracket	—	lieBracketWithin_of_mem_nhds IsOpen.mem_nhds
lieBracketWithin_of_mem_nhds 📖	mathematical	Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	lieBracketWithin lieBracket	—	lieBracketWithin_univ Set.univ_inter lieBracketWithin_inter
lieBracketWithin_of_mem_nhdsWithin 📖	mathematical	Set Filter Filter.instMembership nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup UniqueDiffWithinAt DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule DifferentiableWithinAt	lieBracketWithin	—	fderivWithin_of_mem_nhdsWithin IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
lieBracketWithin_self 📖	mathematical	—	lieBracketWithin Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	sub_self
lieBracketWithin_smul_left 📖	mathematical	DifferentiableWithinAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing UniqueDiffWithinAt DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField	lieBracketWithin SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike fderivWithin	—	lieBracketWithin_swap Pi.neg_apply lieBracketWithin_smul_right add_comm smul_neg neg_add_rev neg_neg neg_smul
lieBracketWithin_smul_right 📖	mathematical	DifferentiableWithinAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing UniqueDiffWithinAt DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField	lieBracketWithin SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike fderivWithin	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsScalarTower.left IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul IsScalarTower.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul fderivWithin_fun_smul add_comm map_smul SemilinearMapClass.toMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass add_sub_assoc smul_sub
lieBracketWithin_subset 📖	mathematical	Set Set.instHasSubset UniqueDiffWithinAt DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace DifferentiableWithinAt	lieBracketWithin	—	lieBracketWithin_of_mem_nhdsWithin nhdsWithin_mono self_mem_nhdsWithin
lieBracketWithin_swap 📖	mathematical	—	lieBracketWithin Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	neg_sub
lieBracketWithin_univ 📖	mathematical	—	lieBracketWithin Set.univ lieBracket	—	fderivWithin_univ
lieBracketWithin_zero_left 📖	mathematical	—	lieBracketWithin Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass fderivWithin_zero sub_self
lieBracketWithin_zero_right 📖	mathematical	—	lieBracketWithin Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	fderivWithin_zero map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass sub_self
lieBracket_add_left 📖	mathematical	DifferentiableAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	lieBracket Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	map_add SemilinearMapClass.toAddHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup fderiv_add ContinuousLinearMap.add_apply Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.const_add_termg
lieBracket_add_right 📖	mathematical	DifferentiableAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	lieBracket Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	map_add SemilinearMapClass.toAddHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup fderiv_add ContinuousLinearMap.add_apply Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.const_add_termg
lieBracket_const_smul_left 📖	mathematical	DifferentiableAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	lieBracket Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid	—	lieBracketWithin_const_smul_left uniqueDiffWithinAt_univ PerfectSpace.not_isolated instPerfectSpace IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul
lieBracket_const_smul_right 📖	mathematical	DifferentiableAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	lieBracket Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid	—	lieBracketWithin_const_smul_right uniqueDiffWithinAt_univ PerfectSpace.not_isolated instPerfectSpace IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul
lieBracket_eq 📖	mathematical	—	lieBracket SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule ContinuousLinearMap.funLike fderiv	—	—
lieBracket_eq_zero_of_eq_zero 📖	mathematical	NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	lieBracket	—	map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass sub_self
lieBracket_fmul_left 📖	mathematical	DifferentiableAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing	lieBracket SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike fderiv	—	lieBracket_smul_left
lieBracket_self 📖	mathematical	—	lieBracket Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	sub_self
lieBracket_smul_left 📖	mathematical	DifferentiableAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing	lieBracket SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike fderiv	—	lieBracket_swap lieBracket_smul_right add_comm smul_neg neg_add_rev neg_neg neg_smul
lieBracket_smul_right 📖	mathematical	DifferentiableAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing	lieBracket SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ContinuousLinearMap.funLike fderiv	—	fderiv_def lieBracketWithin_smul_right uniqueDiffWithinAt_univ PerfectSpace.not_isolated instPerfectSpace IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul
lieBracket_swap 📖	mathematical	—	lieBracket NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	neg_sub
lieBracket_zero_left 📖	mathematical	—	lieBracket Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	lieBracketWithin_zero_left
lieBracket_zero_right 📖	mathematical	—	lieBracket Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	lieBracketWithin_zero_right
pullbackWithin_eq 📖	mathematical	—	pullbackWithin DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule ContinuousLinearMap.funLike ContinuousLinearMap.inverse fderivWithin	—	—
pullbackWithin_eq_of_fderivWithin_eq 📖	mathematical	ContinuousLinearEquiv.toContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule fderivWithin NormedAddCommGroup.toAddCommGroup	pullbackWithin DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike ContinuousLinearEquiv.equivLike ContinuousLinearEquiv.symm	—	RingHomInvPair.ids ContinuousLinearMap.inverse_equiv
pullbackWithin_eq_of_not_isInvertible 📖	mathematical	ContinuousLinearMap.IsInvertible UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule fderivWithin	pullbackWithin NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	ContinuousLinearMap.inverse_of_not_isInvertible
pullbackWithin_lieBracketWithin 📖	mathematical	WithTop ENat Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat minSmoothness instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Nat.instAtLeastTwoHAddOfNat ContDiffWithinAt DifferentiableWithinAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Set Set.instMembership closure interior Set.MapsTo	pullbackWithin lieBracketWithin	—	Nat.instAtLeastTwoHAddOfNat pullbackWithin_lieBracketWithin_of_isSymmSndFDerivWithinAt ContDiffWithinAt.isSymmSndFDerivWithinAt ContDiffWithinAt.of_le LE.le.trans le_minSmoothness
pullbackWithin_lieBracketWithin_of_isSymmSndFDerivWithinAt 📖	mathematical	IsSymmSndFDerivWithinAt ContDiffWithinAt WithTop ENat instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Nat.instAtLeastTwoHAddOfNat DifferentiableWithinAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Set Set.instMembership Set.MapsTo	pullbackWithin lieBracketWithin	—	Nat.instAtLeastTwoHAddOfNat RingHomInvPair.ids RingHomIsometric.ids smulCommClass_self SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomCompTriple.ids exists_continuousLinearEquiv_fderivWithin_symm_eq mem_of_mem_nhdsWithin Filter.EventuallyEq.fderivWithin_eq_of_mem Filter.mp_mem Filter.univ_mem' pullbackWithin_eq_of_fderivWithin_eq ContDiffWithinAt.differentiableWithinAt two_ne_zero CharZero.NeZero.two WithTop.charZero map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousSemilinearEquivClass.continuousSemilinearMapClass ContinuousLinearEquiv.continuousSemilinearEquivClass IsTopologicalAddGroup.toContinuousAdd fderivWithin_clm_apply one_ne_zero NeZero.charZero_one DifferentiableWithinAt.comp ContinuousLinearMap.comp.congr_simp fderivWithin_comp' ContinuousLinearEquiv.apply_symm_apply IsSymmSndFDerivWithinAt.eq add_sub_add_right_eq_sub pullbackWithin_eq_of_not_isInvertible map_zero AddMonoidHomClass.toZeroHomClass ContinuousLinearMap.continuousSemilinearMapClass sub_self
pullbackWithin_lieBracketWithin_of_isSymmSndFDerivWithinAt_of_eventuallyEq 📖	mathematical	IsSymmSndFDerivWithinAt ContDiffWithinAt WithTop ENat instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Nat.instAtLeastTwoHAddOfNat DifferentiableWithinAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Set Set.instMembership Set.MapsTo Filter.EventuallyEq nhds	pullbackWithin lieBracketWithin	—	Nat.instAtLeastTwoHAddOfNat fderivWithin_congr_set Filter.EventuallyEq.symm pullbackWithin_lieBracketWithin_of_isSymmSndFDerivWithinAt IsSymmSndFDerivWithinAt.congr_set ContDiffWithinAt.congr_set Filter.EventuallyEq.lieBracketWithin_vectorField_eq_of_mem nhdsWithin_le_nhds Filter.mp_mem fderivWithin_eventually_congr_set Filter.univ_mem' lieBracketWithin_congr_set
pullbackWithin_univ 📖	mathematical	—	pullbackWithin Set.univ pullback	—	fderivWithin_univ
pullback_eq_of_fderiv_eq 📖	mathematical	ContinuousLinearEquiv.toContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule fderiv NormedAddCommGroup.toAddCommGroup	pullback DFunLike.coe ContinuousLinearEquiv EquivLike.toFunLike ContinuousLinearEquiv.equivLike ContinuousLinearEquiv.symm	—	RingHomInvPair.ids ContinuousLinearMap.inverse_equiv
pullback_eq_of_not_isInvertible 📖	mathematical	ContinuousLinearMap.IsInvertible UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule fderiv	pullback NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	ContinuousLinearMap.inverse_of_not_isInvertible
pullback_lieBracket 📖	mathematical	WithTop ENat Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat minSmoothness instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Nat.instAtLeastTwoHAddOfNat ContDiffAt DifferentiableAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	pullback lieBracket	—	Nat.instAtLeastTwoHAddOfNat pullback_lieBracket_of_isSymmSndFDerivAt ContDiffAt.isSymmSndFDerivAt ContDiffAt.of_le LE.le.trans le_minSmoothness
pullback_lieBracket_of_isSymmSndFDerivAt 📖	mathematical	IsSymmSndFDerivAt ContDiffAt WithTop ENat instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Nat.instAtLeastTwoHAddOfNat DifferentiableAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	pullback lieBracket	—	Nat.instAtLeastTwoHAddOfNat pullbackWithin_lieBracketWithin_of_isSymmSndFDerivWithinAt uniqueDiffOn_univ PerfectSpace.not_isolated instPerfectSpace IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Set.mem_univ Set.mapsTo_univ

VectorField.DifferentiableWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pullbackWithin 📖	mathematical	DifferentiableWithinAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContDiffWithinAt WithTop ENat instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Nat.instAtLeastTwoHAddOfNat ContinuousLinearMap.IsInvertible DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid fderivWithin UniqueDiffOn Set Set.instMembership Set.MapsTo	VectorField.pullbackWithin	—	Nat.instAtLeastTwoHAddOfNat RingHomInvPair.ids RingHomIsometric.ids smulCommClass_self SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomCompTriple.ids exists_continuousLinearEquiv_fderivWithin_symm_eq DifferentiableWithinAt.clm_apply ContDiffWithinAt.differentiableWithinAt one_ne_zero NeZero.charZero_one WithTop.charZero DifferentiableWithinAt.comp two_ne_zero CharZero.NeZero.two DifferentiableWithinAt.congr_of_eventuallyEq Filter.mp_mem Filter.univ_mem' ContinuousLinearMap.inverse_equiv mem_of_mem_nhdsWithin

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_continuousLinearEquiv_fderivWithin_symm_eq 📖	mathematical	ContDiffWithinAt WithTop ENat instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Nat.instAtLeastTwoHAddOfNat ContinuousLinearMap.IsInvertible UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule fderivWithin UniqueDiffOn Set Set.instMembership	ContinuousLinearMap RingHom.id ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing WithTop.one AddMonoidWithOne.toOne ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids ContinuousLinearEquiv.symm Filter.Eventually nhdsWithin DFunLike.coe ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.addCommGroup NormedRing.toRing NormedCommRing.toNormedRing ContinuousLinearMap.module UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul ContinuousLinearMap.funLike ContinuousLinearMap.neg ContinuousLinearMap.comp RingHomCompTriple.ids	—	Nat.instAtLeastTwoHAddOfNat RingHomInvPair.ids RingHomIsometric.ids smulCommClass_self SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomCompTriple.ids ContinuousLinearEquiv.nhds ContDiffWithinAt.continuousWithinAt ContDiffWithinAt.fderivWithin_right le_rfl Filter.mp_mem Filter.univ_mem' mem_of_mem_nhdsWithin ContDiffWithinAt.congr_of_eventuallyEq ContDiffAt.comp_contDiffWithinAt contDiffAt_map_inverse ContinuousLinearMap.inverse_equiv IsTopologicalAddGroup.toContinuousAdd ContinuousLinearMap.topologicalAddGroup ContinuousLinearMap.smulCommClass ContinuousLinearMap.continuousConstSMul ContinuousLinearMap.ext ContinuousLinearEquiv.coe_comp_coe_symm fderivWithin_const_apply ContinuousLinearMap.fderivWithin_of_bilinear ContDiffWithinAt.differentiableWithinAt one_ne_zero NeZero.charZero_one WithTop.charZero ContinuousLinearEquiv.symm_apply_apply ContinuousLinearMap.comp.congr_simp Filter.EventuallyEq.fderivWithin_eq ContinuousLinearMap.comp_neg
exists_continuousLinearEquiv_fderiv_symm_eq 📖	mathematical	ContDiffAt WithTop ENat instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Nat.instAtLeastTwoHAddOfNat ContinuousLinearMap.IsInvertible UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule fderiv	ContinuousLinearMap RingHom.id ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self CommRing.toCommMonoid Field.toCommRing DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing WithTop.one AddMonoidWithOne.toOne ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids ContinuousLinearEquiv.symm Filter.Eventually nhds DFunLike.coe ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.addCommGroup NormedRing.toRing NormedCommRing.toNormedRing ContinuousLinearMap.module UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul ContinuousLinearMap.funLike ContinuousLinearMap.neg ContinuousLinearMap.comp RingHomCompTriple.ids	—	Nat.instAtLeastTwoHAddOfNat RingHomInvPair.ids RingHomIsometric.ids smulCommClass_self SeminormedAddCommGroup.toIsTopologicalAddGroup UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul RingHomCompTriple.ids ContinuousLinearMap.comp.congr_simp exists_continuousLinearEquiv_fderivWithin_symm_eq uniqueDiffOn_univ PerfectSpace.not_isolated instPerfectSpace IsBoundedSMul.continuousSMul Set.mem_univ

---

← Back to Index