LieBracket

📁 Source: Mathlib/Geometry/Manifold/VectorField/LieBracket.lean

Statistics

Metric	Count
Definitions mlieBracket, mlieBracketWithin	2
Theorems mlieBracket_vectorField, mlieBracket_vectorField, mlieBracketWithin_vectorField, mlieBracketWithin_vectorField, mlieBracketWithin_congr_mono, mlieBracketWithin_vectorField, mlieBracketWithin_vectorField', mlieBracketWithin_vectorField_eq, mlieBracketWithin_vectorField_eq_nhds, mlieBracketWithin_vectorField_eq_of_mem, mlieBracketWithin_vectorField_of_insert, mlieBracket_vectorField, mlieBracket_vectorField_eq, differentiableWithinAt_mpullbackWithin_vectorField, leibniz_identity_mlieBracket, leibniz_identity_mlieBracketWithin_apply, leibniz_identity_mlieBracket_apply, mlieBracketWithin_add_left, mlieBracketWithin_add_right, mlieBracketWithin_apply, mlieBracketWithin_congr, mlieBracketWithin_congr', mlieBracketWithin_congr_set, mlieBracketWithin_congr_set', mlieBracketWithin_const_smul_left, mlieBracketWithin_const_smul_right, mlieBracketWithin_def, mlieBracketWithin_eq_lieBracketWithin, mlieBracketWithin_eq_mlieBracket, mlieBracketWithin_eq_zero_of_eq_zero, mlieBracketWithin_eventually_congr_set, mlieBracketWithin_eventually_congr_set', mlieBracketWithin_inter, mlieBracketWithin_of_isOpen, mlieBracketWithin_of_mem_nhds, mlieBracketWithin_of_mem_nhdsWithin, mlieBracketWithin_self, mlieBracketWithin_subset, mlieBracketWithin_swap, mlieBracketWithin_swap_apply, mlieBracketWithin_univ, mlieBracketWithin_zero_left, mlieBracketWithin_zero_right, mlieBracket_add_left, mlieBracket_add_right, mlieBracket_const_smul_left, mlieBracket_const_smul_right, mlieBracket_self, mlieBracket_swap, mlieBracket_swap_apply, mlieBracket_zero_left, mlieBracket_zero_right, mpullbackWithin_mlieBracketWithin, mpullbackWithin_mlieBracketWithin', mpullbackWithin_mlieBracketWithin_of_isSymmSndFDerivWithinAt, mpullback_mlieBracket, mpullback_mlieBracketWithin	57
Total	59

ContDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mlieBracket_vectorField 📖	mathematical	ContMDiff Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle instIsManifoldOfNatWithTopENatOfMinSmoothness_1 instIsManifoldMinSmoothnessOfNatWithTopENat_1 FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle WithTop.some ENat WithTop Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat minSmoothness WithTop.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	VectorField.mlieBracket	—	Nat.instAtLeastTwoHAddOfNat instIsManifoldOfNatWithTopENatOfMinSmoothness_1 instIsManifoldMinSmoothnessOfNatWithTopENat_1 ContMDiffOn.mlieBracketWithin_vectorField uniqueMDiffOn_univ

ContMDiffAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mlieBracket_vectorField 📖	mathematical	ContMDiffAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle instIsManifoldOfNatWithTopENatOfMinSmoothness_1 instIsManifoldMinSmoothnessOfNatWithTopENat_1 FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle WithTop.some ENat WithTop Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat minSmoothness WithTop.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	VectorField.mlieBracket	—	Nat.instAtLeastTwoHAddOfNat instIsManifoldOfNatWithTopENatOfMinSmoothness_1 instIsManifoldMinSmoothnessOfNatWithTopENat_1 ContMDiffWithinAt.mlieBracketWithin_vectorField uniqueMDiffOn_univ Set.mem_univ

ContMDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mlieBracketWithin_vectorField 📖	mathematical	ContMDiffOn Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle instIsManifoldOfNatWithTopENatOfMinSmoothness_1 instIsManifoldMinSmoothnessOfNatWithTopENat_1 FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle WithTop.some ENat UniqueMDiffOn WithTop Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat minSmoothness WithTop.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	VectorField.mlieBracketWithin	—	Nat.instAtLeastTwoHAddOfNat instIsManifoldOfNatWithTopENatOfMinSmoothness_1 instIsManifoldMinSmoothnessOfNatWithTopENat_1 ContMDiffWithinAt.mlieBracketWithin_vectorField

ContMDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mlieBracketWithin_vectorField 📖	mathematical	ContMDiffWithinAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle instIsManifoldOfNatWithTopENatOfMinSmoothness_1 instIsManifoldMinSmoothnessOfNatWithTopENat_1 FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle UniqueMDiffOn Set Set.instMembership WithTop ENat Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat minSmoothness WithTop.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	VectorField.mlieBracketWithin	—	Nat.instAtLeastTwoHAddOfNat instIsManifoldOfNatWithTopENatOfMinSmoothness_1 instIsManifoldMinSmoothnessOfNatWithTopENat_1 le_imp_le_of_le_of_le le_refl add_le_add_left WithTop.addRightMono covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid minSmoothness_add add_assoc minSmoothness_monotone le_add_self WithTop.canonicallyOrderedAdd contMDiffWithinAt_iff_le_ne_infty le_minSmoothness Filter.mp_mem nhdsWithin_le_nhds extChartAt_source_mem_nhds self_mem_nhdsWithin Filter.univ_mem' PartialEquiv.map_source PartialEquiv.left_inv ContDiffWithinAt.lieBracketWithin_vectorField IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfTopWithTopENat instIsManifoldModelSpace contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt VectorField.contMDiffWithinAt_mpullbackWithin_extChartAt_symm le_rfl UniqueMDiffOn.uniqueDiffOn_target_inter ModelWithCorners.target_eq ModelWithCorners.left_inv OpenPartialHomeomorph.left_inv instIsManifoldMinSmoothnessOfNatWithTopENat VectorField.mlieBracketWithin_eq_lieBracketWithin mpullback_vectorField_of_mem_nhdsWithin_of_eq contMDiffAt_extChartAt isInvertible_mfderiv_extChartAt mem_extChartAt_source congr_of_eventuallyEq_of_mem chart_source_mem_nhds VectorField.eventually_contMDiffWithinAt_mpullbackWithin_extChartAt_symm of_le eventually_eventually_nhdsWithin VectorField.eventuallyEq_mpullback_mpullbackWithin_extChartAt VectorField.mpullback_mlieBracketWithin mdifferentiableWithinAt ne_of_gt Right.add_pos_of_nonneg_of_pos zero_le Mathlib.Meta.Positivity.pos_of_isNat WithTop.instIsOrderedRing WithTop.nontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one contMDiffAt_extChartAt' Filter.EventuallyEq.mlieBracketWithin_vectorField_eq_of_mem

DifferentiableWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mlieBracketWithin_congr_mono 📖	mathematical	MDifferentiableWithinAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle IsManifold.instOfNatWithTopENat_1 FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle Set.EqOn UniqueMDiffWithinAt Set Set.instHasSubset	VectorField.mlieBracketWithin	—	Nat.instAtLeastTwoHAddOfNat IsManifold.instOfNatWithTopENat_1 VectorField.mlieBracketWithin_congr VectorField.mlieBracketWithin_subset

Filter.EventuallyEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mlieBracketWithin_vectorField 📖	mathematical	Filter.EventuallyEq nhdsWithin	VectorField.mlieBracketWithin	—	mlieBracketWithin_vectorField' Set.Subset.rfl
mlieBracketWithin_vectorField' 📖	mathematical	Filter.EventuallyEq nhdsWithin Set Set.instHasSubset	VectorField.mlieBracketWithin	—	Filter.mp_mem eventually_eventually_nhdsWithin Filter.univ_mem' mlieBracketWithin_vectorField_eq nhdsWithin_mono
mlieBracketWithin_vectorField_eq 📖	mathematical	Filter.EventuallyEq nhdsWithin	VectorField.mlieBracketWithin	—	lieBracketWithin_vectorField_eq nhdsWithin_mono Set.inter_subset_left Filter.mp_mem ContinuousWithinAt.preimage_mem_nhdsWithin'' ContinuousAt.continuousWithinAt continuousAt_extChartAt_symm ModelWithCorners.left_inv OpenPartialHomeomorph.left_inv Filter.univ_mem' extChartAt_to_inv
mlieBracketWithin_vectorField_eq_nhds 📖	mathematical	Filter.EventuallyEq nhds	VectorField.mlieBracketWithin	—	mlieBracketWithin_vectorField_eq filter_mono nhdsWithin_le_nhds Filter.Eventually.self_of_nhds
mlieBracketWithin_vectorField_eq_of_mem 📖	mathematical	Filter.EventuallyEq nhdsWithin Set Set.instMembership	VectorField.mlieBracketWithin	—	mlieBracketWithin_vectorField_eq mem_of_mem_nhdsWithin
mlieBracketWithin_vectorField_of_insert 📖	mathematical	Filter.EventuallyEq nhdsWithin Set Set.instInsert	VectorField.mlieBracketWithin	—	mem_of_mem_nhdsWithin Set.mem_insert mlieBracketWithin_vectorField' Set.subset_insert
mlieBracket_vectorField 📖	mathematical	Filter.EventuallyEq nhds	VectorField.mlieBracket	—	Filter.mp_mem eventuallyEq_nhds Filter.univ_mem' mlieBracket_vectorField_eq
mlieBracket_vectorField_eq 📖	mathematical	Filter.EventuallyEq nhds	VectorField.mlieBracket	—	VectorField.mlieBracketWithin_univ mlieBracketWithin_vectorField_eq_nhds

MDifferentiableWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
differentiableWithinAt_mpullbackWithin_vectorField 📖	mathematical	MDifferentiableWithinAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle IsManifold.instOfNatWithTopENat_1 FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle	DifferentiableWithinAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule VectorField.mpullbackWithin modelWithCornersSelf chartedSpaceSelf PartialEquiv.toFun PartialEquiv.symm extChartAt Set.range ModelWithCorners.toFun' Set Set.instInter Set.preimage	—	Nat.instAtLeastTwoHAddOfNat IsManifold.instOfNatWithTopENat_1 differentiableWithinAt IsManifold.instOfNatWithTopENat_2 instIsManifoldOfNatWithTopENatOfMinSmoothness IsManifold.instOfTopWithTopENat instIsManifoldModelSpace mpullbackWithin_vectorField_inter_of_eq contMDiffWithinAt_extChartAt_symm_range mem_extChartAt_target isInvertible_mfderivWithin_extChartAt_symm Set.mem_range_self ModelWithCorners.uniqueMDiffOn le_rfl extChartAt_to_inv Set.inter_comm MDifferentiableAt.comp_mdifferentiableWithinAt ContMDiffAt.mdifferentiableAt ContMDiff.contMDiffAt contMDiff_snd_tangentBundle_modelSpace one_ne_zero NeZero.charZero_one WithTop.charZero

VectorField

Definitions

Name	Category	Theorems
mlieBracket 📖	CompOp	24 math math: AddGroupLieAlgebra.bracket_def, mlieBracket_zero_right, mulInvariantVector_mlieBracket, Filter.EventuallyEq.mlieBracket_vectorField_eq, mlieBracketWithin_of_isOpen, mlieBracketWithin_of_mem_nhds, mpullback_mlieBracket, leibniz_identity_mlieBracket, mlieBracket_add_right, mlieBracketWithin_univ, leibniz_identity_mlieBracket_apply, mlieBracket_zero_left, mlieBracket_swap_apply, ContMDiffAt.mlieBracket_vectorField, Filter.EventuallyEq.mlieBracket_vectorField, mlieBracket_add_left, mlieBracket_const_smul_left, ContDiff.mlieBracket_vectorField, addInvariantVector_mlieBracket, mlieBracketWithin_eq_mlieBracket, mlieBracket_swap, GroupLieAlgebra.bracket_def, mlieBracket_self, mlieBracket_const_smul_right
mlieBracketWithin 📖	CompOp	40 math math: ContMDiffOn.mlieBracketWithin_vectorField, ContMDiffWithinAt.mlieBracketWithin_vectorField, mlieBracketWithin_congr_set, mlieBracketWithin_congr_set', mpullback_mlieBracketWithin, mlieBracketWithin_inter, mlieBracketWithin_const_smul_right, DifferentiableWithinAt.mlieBracketWithin_congr_mono, mlieBracketWithin_of_mem_nhdsWithin, mpullbackWithin_mlieBracketWithin', mlieBracketWithin_eventually_congr_set, Filter.EventuallyEq.mlieBracketWithin_vectorField', mlieBracketWithin_of_isOpen, mlieBracketWithin_of_mem_nhds, mlieBracketWithin_const_smul_left, mlieBracketWithin_congr, mlieBracketWithin_zero_right, mlieBracketWithin_def, mlieBracketWithin_eq_zero_of_eq_zero, mlieBracketWithin_add_left, mlieBracketWithin_univ, mlieBracketWithin_self, mlieBracketWithin_subset, mlieBracketWithin_swap_apply, mlieBracketWithin_add_right, Filter.EventuallyEq.mlieBracketWithin_vectorField_eq, Filter.EventuallyEq.mlieBracketWithin_vectorField_of_insert, mlieBracketWithin_eventually_congr_set', leibniz_identity_mlieBracketWithin_apply, mpullbackWithin_mlieBracketWithin, mlieBracketWithin_eq_mlieBracket, mpullbackWithin_mlieBracketWithin_of_isSymmSndFDerivWithinAt, Filter.EventuallyEq.mlieBracketWithin_vectorField_eq_of_mem, Filter.EventuallyEq.mlieBracketWithin_vectorField, mlieBracketWithin_apply, mlieBracketWithin_eq_lieBracketWithin, Filter.EventuallyEq.mlieBracketWithin_vectorField_eq_nhds, mlieBracketWithin_zero_left, mlieBracketWithin_swap, mlieBracketWithin_congr'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
leibniz_identity_mlieBracket 📖	mathematical	ContMDiff Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle instIsManifoldOfNatWithTopENatOfMinSmoothness_1 instIsManifoldMinSmoothnessOfNatWithTopENat_1 instIsManifoldMinSmoothnessOfNatWithTopENat FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle minSmoothness WithTop ENat instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Nat.instAtLeastTwoHAddOfNat	mlieBracket Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	Nat.instAtLeastTwoHAddOfNat instIsManifoldOfNatWithTopENatOfMinSmoothness_1 instIsManifoldMinSmoothnessOfNatWithTopENat_1 instIsManifoldMinSmoothnessOfNatWithTopENat leibniz_identity_mlieBracket_apply
leibniz_identity_mlieBracketWithin_apply 📖	mathematical	UniqueMDiffOn Set Set.instMembership closure interior ContMDiffWithinAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle instIsManifoldOfNatWithTopENatOfMinSmoothness_1 instIsManifoldMinSmoothnessOfNatWithTopENat_1 instIsManifoldMinSmoothnessOfNatWithTopENat FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle minSmoothness WithTop ENat instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Nat.instAtLeastTwoHAddOfNat	mlieBracketWithin AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	Nat.instAtLeastTwoHAddOfNat instIsManifoldOfNatWithTopENatOfMinSmoothness_1 instIsManifoldMinSmoothnessOfNatWithTopENat_1 instIsManifoldMinSmoothnessOfNatWithTopENat le_rfl Filter.inter_mem self_mem_nhdsWithin nhdsWithin_le_nhds extChartAt_source_mem_nhds Filter.mp_mem Filter.univ_mem' PartialEquiv.map_source PartialEquiv.left_inv IsManifold.instOfTopWithTopENat instIsManifoldModelSpace contMDiffWithinAt_mpullbackWithin_extChartAt_symm eventually_contMDiffWithinAt_mpullbackWithin_extChartAt_symm eventuallyEq_mpullback_mpullbackWithin_extChartAt Filter.EventuallyEq.mlieBracketWithin_vectorField_eq_of_mem Filter.EventuallyEq.mlieBracketWithin_vectorField chart_source_mem_nhds eventually_eventually_nhdsWithin mpullback_mlieBracketWithin ContMDiffWithinAt.mdifferentiableWithinAt LT.lt.ne' LT.lt.trans_le two_pos WithTop.zeroLEOneClass IsOrderedRing.toZeroLEOneClass NeZero.charZero_one WithTop.charZero WithTop.addLeftMono IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid le_minSmoothness contMDiffAt_extChartAt' Filter.EventuallyEq.rfl ContMDiffWithinAt.mlieBracketWithin_vectorField UniqueMDiffOn.uniqueMDiffOn_target_inter mem_extChartAt_target ModelWithCorners.left_inv OpenPartialHomeomorph.left_inv one_ne_zero contMDiffAt_extChartAt mpullback_add_apply mpullback_apply mlieBracketWithin_eq_lieBracketWithin leibniz_identity_lieBracketWithin UniqueMDiffOn.uniqueDiffOn_target_inter Set.inter_comm extChartAt_mem_closure_interior mem_extChartAt_source IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt
leibniz_identity_mlieBracket_apply 📖	mathematical	ContMDiffAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle instIsManifoldOfNatWithTopENatOfMinSmoothness_1 instIsManifoldMinSmoothnessOfNatWithTopENat_1 instIsManifoldMinSmoothnessOfNatWithTopENat FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle minSmoothness WithTop ENat instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Nat.instAtLeastTwoHAddOfNat	mlieBracket AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	Nat.instAtLeastTwoHAddOfNat instIsManifoldOfNatWithTopENatOfMinSmoothness_1 instIsManifoldMinSmoothnessOfNatWithTopENat_1 instIsManifoldMinSmoothnessOfNatWithTopENat leibniz_identity_mlieBracketWithin_apply uniqueMDiffOn_univ interior_univ IsClosed.closure_eq Set.mem_univ
mlieBracketWithin_add_left 📖	mathematical	MDifferentiableWithinAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle IsManifold.instOfNatWithTopENat_1 FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle UniqueMDiffWithinAt	mlieBracketWithin Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	Nat.instAtLeastTwoHAddOfNat IsManifold.instOfNatWithTopENat_1 map_add SemilinearMapClass.toAddHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass mpullbackWithin_add lieBracketWithin_add_left MDifferentiableWithinAt.differentiableWithinAt_mpullbackWithin_vectorField uniqueMDiffWithinAt_iff_inter_range
mlieBracketWithin_add_right 📖	mathematical	MDifferentiableWithinAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle IsManifold.instOfNatWithTopENat_1 FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle UniqueMDiffWithinAt	mlieBracketWithin Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	Nat.instAtLeastTwoHAddOfNat IsManifold.instOfNatWithTopENat_1 mlieBracketWithin_swap Pi.neg_apply mlieBracketWithin_add_left Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.term_neg neg_zero
mlieBracketWithin_apply 📖	mathematical	—	mlieBracketWithin DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring TangentSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf PartialEquiv.toFun extChartAt instTopologicalSpaceTangentSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instModuleTangentSpace ContinuousLinearMap.funLike ContinuousLinearMap.inverse mfderiv lieBracketWithin mpullbackWithin PartialEquiv.symm Set.range ModelWithCorners.toFun' Set Set.instInter Set.preimage	—	—
mlieBracketWithin_congr 📖	mathematical	Set.EqOn	mlieBracketWithin	—	Filter.EventuallyEq.mlieBracketWithin_vectorField_eq Filter.EventuallyEq.filter_mono Set.EqOn.eventuallyEq inf_le_right
mlieBracketWithin_congr' 📖	mathematical	Set.EqOn Set Set.instMembership	mlieBracketWithin	—	mlieBracketWithin_congr
mlieBracketWithin_congr_set 📖	mathematical	Filter.EventuallyEq nhds	mlieBracketWithin	—	mlieBracketWithin_congr_set' Filter.EventuallyEq.filter_mono inf_le_left
mlieBracketWithin_congr_set' 📖	mathematical	Filter.EventuallyEq nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet	mlieBracketWithin	—	preimage_extChartAt_eventuallyEq_compl_singleton lieBracketWithin_congr_set'
mlieBracketWithin_const_smul_left 📖	mathematical	MDifferentiableWithinAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle IsManifold.instOfNatWithTopENat_1 FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle UniqueMDiffWithinAt	mlieBracketWithin Pi.instSMul SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroupTangentSpace DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid instModuleTangentSpace AddZero.toZero AddZeroClass.toAddZero ENormedAddMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toENormedAddMonoid	—	Nat.instAtLeastTwoHAddOfNat IsManifold.instOfNatWithTopENat_1 map_smul SemilinearMapClass.toMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass mpullbackWithin_smul lieBracketWithin_const_smul_left MDifferentiableWithinAt.differentiableWithinAt_mpullbackWithin_vectorField uniqueMDiffWithinAt_iff_inter_range
mlieBracketWithin_const_smul_right 📖	mathematical	MDifferentiableWithinAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle IsManifold.instOfNatWithTopENat_1 FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle UniqueMDiffWithinAt	mlieBracketWithin Pi.instSMul SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroupTangentSpace DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid instModuleTangentSpace AddZero.toZero AddZeroClass.toAddZero ENormedAddMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toENormedAddMonoid	—	Nat.instAtLeastTwoHAddOfNat IsManifold.instOfNatWithTopENat_1 map_smul SemilinearMapClass.toMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass mpullbackWithin_smul lieBracketWithin_const_smul_right MDifferentiableWithinAt.differentiableWithinAt_mpullbackWithin_vectorField uniqueMDiffWithinAt_iff_inter_range
mlieBracketWithin_def 📖	mathematical	—	mlieBracketWithin mpullback UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf PartialEquiv.toFun extChartAt lieBracketWithin mpullbackWithin PartialEquiv.symm Set.range ModelWithCorners.toFun' Set Set.instInter Set.preimage	—	—
mlieBracketWithin_eq_lieBracketWithin 📖	mathematical	—	mlieBracketWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf lieBracketWithin	—	mfderiv_id ContinuousLinearMap.inverse_id PartialEquiv.trans_refl Set.range_id mpullbackWithin_univ mpullback_id Set.inter_univ
mlieBracketWithin_eq_mlieBracket 📖	mathematical	UniqueMDiffWithinAt MDifferentiableAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle IsManifold.instOfNatWithTopENat_1 FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle	mlieBracketWithin mlieBracket	—	Nat.instAtLeastTwoHAddOfNat IsManifold.instOfNatWithTopENat_1 mlieBracketWithin_subset Set.subset_univ
mlieBracketWithin_eq_zero_of_eq_zero 📖	mathematical	TangentSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroupTangentSpace	mlieBracketWithin	—	lieBracketWithin_eq_zero_of_eq_zero ModelWithCorners.left_inv OpenPartialHomeomorph.left_inv map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass
mlieBracketWithin_eventually_congr_set 📖	mathematical	Filter.EventuallyEq nhds	mlieBracketWithin	—	mlieBracketWithin_eventually_congr_set' Filter.EventuallyEq.filter_mono inf_le_left
mlieBracketWithin_eventually_congr_set' 📖	mathematical	Filter.EventuallyEq nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet	nhds mlieBracketWithin	—	Filter.Eventually.mono eventually_nhds_nhdsWithin mlieBracketWithin_congr_set'
mlieBracketWithin_inter 📖	mathematical	Set Filter Filter.instMembership nhds	mlieBracketWithin Set.instInter	—	mlieBracketWithin_congr_set Filter.mp_mem Filter.univ_mem'
mlieBracketWithin_of_isOpen 📖	mathematical	IsOpen Set Set.instMembership	mlieBracketWithin mlieBracket	—	mlieBracketWithin_of_mem_nhds IsOpen.mem_nhds
mlieBracketWithin_of_mem_nhds 📖	mathematical	Set Filter Filter.instMembership nhds	mlieBracketWithin mlieBracket	—	mlieBracketWithin_univ Set.univ_inter mlieBracketWithin_inter
mlieBracketWithin_of_mem_nhdsWithin 📖	mathematical	Set Filter Filter.instMembership nhdsWithin UniqueMDiffWithinAt MDifferentiableWithinAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle IsManifold.instOfNatWithTopENat_1 FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle	mlieBracketWithin	—	Nat.instAtLeastTwoHAddOfNat IsManifold.instOfNatWithTopENat_1 lieBracketWithin_of_mem_nhdsWithin Filter.inter_mem nhdsWithin_mono Set.inter_subset_left ContinuousWithinAt.preimage_mem_nhdsWithin'' ContinuousAt.continuousWithinAt continuousAt_extChartAt_symm ModelWithCorners.left_inv OpenPartialHomeomorph.left_inv Set.inter_subset_right self_mem_nhdsWithin uniqueMDiffWithinAt_iff_inter_range MDifferentiableWithinAt.differentiableWithinAt_mpullbackWithin_vectorField
mlieBracketWithin_self 📖	mathematical	—	mlieBracketWithin Pi.instZero Set TangentSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroupTangentSpace	—	lieBracketWithin_self map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass
mlieBracketWithin_subset 📖	mathematical	Set Set.instHasSubset UniqueMDiffWithinAt MDifferentiableWithinAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle IsManifold.instOfNatWithTopENat_1 FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle	mlieBracketWithin	—	Nat.instAtLeastTwoHAddOfNat IsManifold.instOfNatWithTopENat_1 mlieBracketWithin_of_mem_nhdsWithin nhdsWithin_mono self_mem_nhdsWithin
mlieBracketWithin_swap 📖	mathematical	—	mlieBracketWithin Pi.instNeg TangentSpace NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroupTangentSpace	—	mlieBracketWithin_swap_apply
mlieBracketWithin_swap_apply 📖	mathematical	—	mlieBracketWithin TangentSpace NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroupTangentSpace	—	mlieBracketWithin.eq_1 lieBracketWithin_swap mpullback_neg
mlieBracketWithin_univ 📖	mathematical	—	mlieBracketWithin Set.univ mlieBracket	—	—
mlieBracketWithin_zero_left 📖	mathematical	—	mlieBracketWithin Pi.instZero TangentSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroupTangentSpace	—	mpullbackWithin_zero lieBracketWithin_zero_left mpullback_zero
mlieBracketWithin_zero_right 📖	mathematical	—	mlieBracketWithin Pi.instZero TangentSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroupTangentSpace	—	mlieBracketWithin_swap mlieBracketWithin_zero_left neg_zero
mlieBracket_add_left 📖	mathematical	MDifferentiableAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle IsManifold.instOfNatWithTopENat_1 FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle	mlieBracket Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	Nat.instAtLeastTwoHAddOfNat IsManifold.instOfNatWithTopENat_1 mlieBracketWithin_add_left uniqueMDiffWithinAt_univ
mlieBracket_add_right 📖	mathematical	MDifferentiableAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle IsManifold.instOfNatWithTopENat_1 FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle	mlieBracket Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid	—	Nat.instAtLeastTwoHAddOfNat IsManifold.instOfNatWithTopENat_1 mlieBracketWithin_add_right uniqueMDiffWithinAt_univ
mlieBracket_const_smul_left 📖	mathematical	MDifferentiableAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle IsManifold.instOfNatWithTopENat_1 FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle	mlieBracket Pi.instSMul SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroupTangentSpace DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid instModuleTangentSpace AddZero.toZero AddZeroClass.toAddZero ENormedAddMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toENormedAddMonoid	—	Nat.instAtLeastTwoHAddOfNat IsManifold.instOfNatWithTopENat_1 mlieBracketWithin_const_smul_left uniqueMDiffWithinAt_univ
mlieBracket_const_smul_right 📖	mathematical	MDifferentiableAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle IsManifold.instOfNatWithTopENat_1 FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle	mlieBracket Pi.instSMul SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroupTangentSpace DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid instModuleTangentSpace AddZero.toZero AddZeroClass.toAddZero ENormedAddMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toENormedAddMonoid	—	Nat.instAtLeastTwoHAddOfNat IsManifold.instOfNatWithTopENat_1 mlieBracketWithin_const_smul_right uniqueMDiffWithinAt_univ
mlieBracket_self 📖	mathematical	—	mlieBracket Pi.instZero TangentSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroupTangentSpace	—	mlieBracketWithin_self
mlieBracket_swap 📖	mathematical	—	mlieBracket Pi.instNeg TangentSpace NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroupTangentSpace	—	mlieBracketWithin_swap
mlieBracket_swap_apply 📖	mathematical	—	mlieBracket TangentSpace NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroupTangentSpace	—	mlieBracketWithin_swap_apply
mlieBracket_zero_left 📖	mathematical	—	mlieBracket Pi.instZero TangentSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroupTangentSpace	—	mlieBracketWithin_zero_left
mlieBracket_zero_right 📖	mathematical	—	mlieBracket Pi.instZero TangentSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroupTangentSpace	—	mlieBracketWithin_zero_right
mpullbackWithin_mlieBracketWithin 📖	mathematical	MDifferentiableWithinAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle instIsManifoldOfNatWithTopENatOfMinSmoothness_1 instIsManifoldMinSmoothnessOfNatWithTopENat_1 FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle UniqueMDiffOn ContMDiffWithinAt Set Set.instMembership 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 Filter Filter.instMembership nhdsWithin Set.preimage closure interior	mpullbackWithin mlieBracketWithin	—	Nat.instAtLeastTwoHAddOfNat instIsManifoldOfNatWithTopENatOfMinSmoothness_1 instIsManifoldMinSmoothnessOfNatWithTopENat_1 mpullbackWithin_mlieBracketWithin' Set.Subset.rfl
mpullbackWithin_mlieBracketWithin' 📖	mathematical	MDifferentiableWithinAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle instIsManifoldOfNatWithTopENatOfMinSmoothness_1 instIsManifoldMinSmoothnessOfNatWithTopENat_1 FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle UniqueMDiffOn ContMDiffWithinAt Set Set.instMembership 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 Filter Filter.instMembership nhdsWithin Set.preimage closure interior Set.instHasSubset	mpullbackWithin mlieBracketWithin	—	Nat.instAtLeastTwoHAddOfNat instIsManifoldOfNatWithTopENatOfMinSmoothness_1 instIsManifoldMinSmoothnessOfNatWithTopENat_1 ContDiffWithinAt.congr_set contMDiffWithinAt_iff Filter.EventuallyEq.inter Filter.EventuallyEq.refl Filter.EventuallyEq.symm extChartAt_target_eventuallyEq mpullbackWithin_mlieBracketWithin_of_isSymmSndFDerivWithinAt instIsManifoldOfNatWithTopENatOfMinSmoothness ContMDiffWithinAt.of_le ContMDiffWithinAt.mono LE.le.trans le_minSmoothness IsSymmSndFDerivWithinAt.congr_set ContDiffWithinAt.isSymmSndFDerivWithinAt ContDiffWithinAt.of_le le_rfl Set.inter_comm UniqueMDiffOn.uniqueDiffOn_target_inter extChartAt_mem_closure_interior mem_extChartAt_source ModelWithCorners.target_eq ModelWithCorners.left_inv OpenPartialHomeomorph.left_inv IsSymmSndFDerivWithinAt.mono_of_mem_nhdsWithin Filter.mem_of_superset self_mem_nhdsWithin Set.inter_subset_inter_left Set.preimage_mono
mpullbackWithin_mlieBracketWithin_of_isSymmSndFDerivWithinAt 📖	mathematical	MDifferentiableWithinAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle IsManifold.instOfNatWithTopENat_1 FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle UniqueMDiffOn ContMDiffWithinAt WithTop ENat instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Nat.instAtLeastTwoHAddOfNat Set Set.instMembership Filter Filter.instMembership nhdsWithin Set.preimage IsSymmSndFDerivWithinAt PartialEquiv.toFun extChartAt PartialEquiv.symm Set.instInter Set.range ModelWithCorners.toFun'	mpullbackWithin mlieBracketWithin	—	Nat.instAtLeastTwoHAddOfNat IsManifold.instOfNatWithTopENat_1 ModelWithCorners.left_inv OpenPartialHomeomorph.left_inv RingHomInvPair.ids completeSpace_congr ContinuousLinearEquiv.isUniformEmbedding SeminormedAddCommGroup.to_isUniformAddGroup ContMDiffWithinAt.contMDiffOn' le_rfl ContinuousWithinAt.preimage_mem_nhdsWithin ContMDiffWithinAt.continuousWithinAt extChartAt_source_mem_nhds mem_nhdsWithin Filter.inter_mem IsOpen.inter Set.Subset.trans HasSubset.Subset.trans Set.instIsTransSubset Set.inter_subset_left Set.inter_subset_right ContMDiffOn.mono Set.subset_insert IsOpen.mem_nhds Filter.mp_mem Filter.univ_mem' mfderivWithin_inter mlieBracketWithin_inter MDifferentiableWithinAt.mono UniqueMDiffOn.inter IsSymmSndFDerivWithinAt.congr_set ContinuousAt.preimage_mem_nhds continuousAt_extChartAt_symm Filter.EventuallyEq.mlieBracketWithin_vectorField_eq_of_mem nhdsWithin_le_nhds mfderivWithin_eventually_congr_set ContinuousLinearMap.inverse_of_not_isInvertible lieBracketWithin_eq_zero_of_eq_zero map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass
mpullback_mlieBracket 📖	mathematical	MDifferentiableAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle instIsManifoldOfNatWithTopENatOfMinSmoothness_1 instIsManifoldMinSmoothnessOfNatWithTopENat_1 FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle ContMDiffAt 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	mpullback mlieBracket	—	Nat.instAtLeastTwoHAddOfNat instIsManifoldOfNatWithTopENatOfMinSmoothness_1 instIsManifoldMinSmoothnessOfNatWithTopENat_1 mpullback_mlieBracketWithin uniqueMDiffOn_univ Set.mem_univ nhdsWithin_univ
mpullback_mlieBracketWithin 📖	mathematical	MDifferentiableWithinAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle instIsManifoldOfNatWithTopENatOfMinSmoothness_1 instIsManifoldMinSmoothnessOfNatWithTopENat_1 FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle UniqueMDiffOn ContMDiffAt Set Set.instMembership 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 Filter Filter.instMembership nhdsWithin Set.preimage	mpullback mlieBracketWithin	—	Nat.instAtLeastTwoHAddOfNat instIsManifoldOfNatWithTopENatOfMinSmoothness_1 instIsManifoldMinSmoothnessOfNatWithTopENat_1 mfderivWithin_eq_mfderiv ContMDiffAt.mdifferentiableAt LT.lt.ne' LT.lt.trans_le two_pos WithTop.zeroLEOneClass IsOrderedRing.toZeroLEOneClass NeZero.charZero_one WithTop.charZero WithTop.addLeftMono IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid LE.le.trans le_minSmoothness mpullbackWithin_mlieBracketWithin' uniqueMDiffOn_univ ContMDiffAt.contMDiffWithinAt interior_univ IsClosed.closure_eq Set.subset_univ Filter.EventuallyEq.mlieBracketWithin_vectorField_of_insert Set.insert_eq_of_mem Filter.mp_mem self_mem_nhdsWithin nhdsWithin_le_nhds contMDiffAt_iff_contMDiffAt_nhds instIsManifoldOfNatWithTopENatOfMinSmoothness ContMDiffAt.of_le Filter.univ_mem' two_ne_zero CharZero.NeZero.two

---

← Back to Index