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`, `mfderiv_extChartAt_inverse_comp_mfderivWithin_extChartAT_symm`, `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_smul_left`, `mlieBracketWithin_smul_right`, `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_smul_left`, `mlieBracket_smul_right`, `mlieBracket_swap`, `mlieBracket_swap_apply`, `mlieBracket_zero_left`, `mlieBracket_zero_right`, `mpullbackWithin_mlieBracketWithin`, `mpullbackWithin_mlieBracketWithin'`, `mpullbackWithin_mlieBracketWithin_of_isSymmSndFDerivWithinAt`, `mpullback_mfderivWithin_apply_smul`, `mpullback_mlieBracket`, `mpullback_mlieBracketWithin`	63
Total	65

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.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `instIsManifoldOfNatWithTopENatOfMinSmoothness_1` `instIsManifoldMinSmoothnessOfNatWithTopENat_1` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `WithTop.some` `ENat` `Bundle.TotalSpace.mk'` `WithTop` `Preorder.toLE` `WithTop.instPreorder` `instPreorderENat` `minSmoothness` `WithTop.add` `instAddENat` `WithTop.one` `AddMonoidWithOne.toOne` `instAddMonoidWithOneENat`	`ContMDiff` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `instIsManifoldOfNatWithTopENatOfMinSmoothness_1` `instIsManifoldMinSmoothnessOfNatWithTopENat_1` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `WithTop.some` `ENat` `Bundle.TotalSpace.mk'` `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.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `instIsManifoldOfNatWithTopENatOfMinSmoothness_1` `instIsManifoldMinSmoothnessOfNatWithTopENat_1` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `WithTop.some` `ENat` `Bundle.TotalSpace.mk'` `WithTop` `Preorder.toLE` `WithTop.instPreorder` `instPreorderENat` `minSmoothness` `WithTop.add` `instAddENat` `WithTop.one` `AddMonoidWithOne.toOne` `instAddMonoidWithOneENat`	`ContMDiffAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `instIsManifoldOfNatWithTopENatOfMinSmoothness_1` `instIsManifoldMinSmoothnessOfNatWithTopENat_1` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `WithTop.some` `ENat` `Bundle.TotalSpace.mk'` `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.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `instIsManifoldOfNatWithTopENatOfMinSmoothness_1` `instIsManifoldMinSmoothnessOfNatWithTopENat_1` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `WithTop.some` `ENat` `Bundle.TotalSpace.mk'` `UniqueMDiffOn` `WithTop` `Preorder.toLE` `WithTop.instPreorder` `instPreorderENat` `minSmoothness` `WithTop.add` `instAddENat` `WithTop.one` `AddMonoidWithOne.toOne` `instAddMonoidWithOneENat`	`ContMDiffOn` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `instIsManifoldOfNatWithTopENatOfMinSmoothness_1` `instIsManifoldMinSmoothnessOfNatWithTopENat_1` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `WithTop.some` `ENat` `Bundle.TotalSpace.mk'` `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.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `instIsManifoldOfNatWithTopENatOfMinSmoothness_1` `instIsManifoldMinSmoothnessOfNatWithTopENat_1` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `Bundle.TotalSpace.mk'` `UniqueMDiffOn` `Set` `Set.instMembership` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `instPreorderENat` `minSmoothness` `WithTop.add` `instAddENat` `WithTop.one` `AddMonoidWithOne.toOne` `instAddMonoidWithOneENat`	`ContMDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `instIsManifoldOfNatWithTopENatOfMinSmoothness_1` `instIsManifoldMinSmoothnessOfNatWithTopENat_1` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `Bundle.TotalSpace.mk'` `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.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `IsManifold.instOfNatWithTopENat_1` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `Bundle.TotalSpace.mk'` `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`	`Filter.EventuallyEq` `nhdsWithin` `VectorField.mlieBracketWithin`	—	`mlieBracketWithin_vectorField'` `Set.Subset.rfl`
`mlieBracketWithin_vectorField'` 📖	mathematical	`Filter.EventuallyEq` `nhdsWithin` `Set` `Set.instHasSubset`	`Filter.EventuallyEq` `nhdsWithin` `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`	`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.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `IsManifold.instOfNatWithTopENat_1` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle`	`DifferentiableWithinAt` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `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	31 math math: `AddGroupLieAlgebra.bracket_def`, `mlieBracket_smul_left`, `mlieBracket_zero_right`, `mulInvariantVector_mlieBracket`, `Filter.EventuallyEq.mlieBracket_vectorField_eq`, `CovariantDerivative.torsion_apply`, `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`, `CovariantDerivative.torsion_eq_zero_iff`, `mlieBracket_const_smul_left`, `ContDiff.mlieBracket_vectorField`, `addInvariantVector_mlieBracket`, `mlieBracketWithin_eq_mlieBracket`, `IsCovariantDerivativeOn.torsion_apply_eq_extend`, `mlieBracket_swap`, `CovariantDerivative.torsion_apply_eq_extend`, `GroupLieAlgebra.bracket_def`, `IsCovariantDerivativeOn.torsion_apply`, `mlieBracket_self`, `mlieBracket_smul_right`, `mlieBracket_const_smul_right`
`mlieBracketWithin` 📖	CompOp	42 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_smul_left`, `mlieBracketWithin_self`, `mlieBracketWithin_smul_right`, `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.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `instIsManifoldOfNatWithTopENatOfMinSmoothness_1` `instIsManifoldMinSmoothnessOfNatWithTopENat_1` `instIsManifoldMinSmoothnessOfNatWithTopENat` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `minSmoothness` `WithTop` `ENat` `instOfNatAtLeastTwo` `WithTop.natCast` `ENat.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Bundle.TotalSpace.mk'`	`mlieBracket` `Pi.instAdd` `TangentSpace` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `instTopologicalSpaceTangentSpace` `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.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `instIsManifoldOfNatWithTopENatOfMinSmoothness_1` `instIsManifoldMinSmoothnessOfNatWithTopENat_1` `instIsManifoldMinSmoothnessOfNatWithTopENat` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `minSmoothness` `WithTop` `ENat` `instOfNatAtLeastTwo` `WithTop.natCast` `ENat.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Bundle.TotalSpace.mk'`	`mlieBracketWithin` `TangentSpace` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `instTopologicalSpaceTangentSpace` `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` `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.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `instIsManifoldOfNatWithTopENatOfMinSmoothness_1` `instIsManifoldMinSmoothnessOfNatWithTopENat_1` `instIsManifoldMinSmoothnessOfNatWithTopENat` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `minSmoothness` `WithTop` `ENat` `instOfNatAtLeastTwo` `WithTop.natCast` `ENat.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Bundle.TotalSpace.mk'`	`mlieBracket` `TangentSpace` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `instTopologicalSpaceTangentSpace` `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`
`mfderiv_extChartAt_inverse_comp_mfderivWithin_extChartAT_symm` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `PartialEquiv.toFun` `PartialEquiv.symm` `extChartAt` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `ContinuousLinearMap.funLike` `ContinuousLinearMap.comp` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `RingHomCompTriple.ids` `ContinuousLinearMap.inverse` `mfderiv` `mfderivWithin` `Set.range` `ModelWithCorners.toFun'`	—	`Nat.instAtLeastTwoHAddOfNat` `RingHomCompTriple.ids` `extChartAt_to_inv` `ContinuousLinearMap.IsInvertible.inverse_comp_of_left` `isInvertible_mfderivWithin_extChartAt_symm` `IsManifold.instOfNatWithTopENat_1` `mem_extChartAt_target` `ContinuousLinearMap.inverse_id` `mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt'` `mem_extChartAt_source`
`mlieBracketWithin_add_left` 📖	mathematical	`MDifferentiableWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `IsManifold.instOfNatWithTopENat_1` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `Bundle.TotalSpace.mk'` `UniqueMDiffWithinAt`	`mlieBracketWithin` `Pi.instAdd` `TangentSpace` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `instTopologicalSpaceTangentSpace` `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.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `IsManifold.instOfNatWithTopENat_1` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `Bundle.TotalSpace.mk'` `UniqueMDiffWithinAt`	`mlieBracketWithin` `Pi.instAdd` `TangentSpace` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `instTopologicalSpaceTangentSpace` `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.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `IsManifold.instOfNatWithTopENat_1` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `Bundle.TotalSpace.mk'` `UniqueMDiffWithinAt`	`mlieBracketWithin` `Pi.instSMul` `TangentSpace` `SMulZeroClass.toSMul` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupTangentSpace` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `instModuleTangentSpace` `AddZero.toZero` `AddZeroClass.toAddZero` `ENormedAddMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toENormedAddMonoid`	—	`Nat.instAtLeastTwoHAddOfNat` `IsManifold.instOfNatWithTopENat_1` `RingHomInvPair.ids` `mfderivWithin_const` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousSemilinearEquivClass.continuousSemilinearMapClass` `ContinuousLinearEquiv.continuousSemilinearEquivClass` `neg_zero` `zero_smul` `zero_add` `mlieBracketWithin_smul_left` `mdifferentiableWithinAt_const`
`mlieBracketWithin_const_smul_right` 📖	mathematical	`MDifferentiableWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `IsManifold.instOfNatWithTopENat_1` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `Bundle.TotalSpace.mk'` `UniqueMDiffWithinAt`	`mlieBracketWithin` `Pi.instSMul` `TangentSpace` `SMulZeroClass.toSMul` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupTangentSpace` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `instModuleTangentSpace` `AddZero.toZero` `AddZeroClass.toAddZero` `ENormedAddMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toENormedAddMonoid`	—	`Nat.instAtLeastTwoHAddOfNat` `IsManifold.instOfNatWithTopENat_1` `RingHomInvPair.ids` `mfderivWithin_const` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousSemilinearEquivClass.continuousSemilinearMapClass` `ContinuousLinearEquiv.continuousSemilinearEquivClass` `zero_smul` `zero_add` `mlieBracketWithin_smul_right` `mdifferentiableWithinAt_const`
`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.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `IsManifold.instOfNatWithTopENat_1` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `Bundle.TotalSpace.mk'`	`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` `TangentSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupTangentSpace`	—	`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`	`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`	`Filter.EventuallyEq` `nhds` `mlieBracketWithin`	—	`Filter.Eventually.mono` `eventually_nhds_nhdsWithin` `mlieBracketWithin_congr_set'`
`mlieBracketWithin_inter` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds`	`mlieBracketWithin` `Set` `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.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `IsManifold.instOfNatWithTopENat_1` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `Bundle.TotalSpace.mk'`	`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_smul_left` 📖	mathematical	`MDifferentiableWithinAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `modelWithCornersSelf` `chartedSpaceSelf` `Prod.normedAddCommGroup` `Prod.normedSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `IsManifold.instOfNatWithTopENat_1` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `UniqueMDiffWithinAt`	`mlieBracketWithin` `Pi.smul'` `TangentSpace` `SMulZeroClass.toSMul` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupTangentSpace` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `instModuleTangentSpace` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddZero.toZero` `AddZeroClass.toAddZero` `ENormedAddMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toENormedAddMonoid` `NegZeroClass.toNeg` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DFunLike.coe` `ContinuousLinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NormedField.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `NormedSpace.toModule` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `NormedSpace.fromTangentSpace` `ContinuousLinearMap` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ContinuousLinearMap.funLike` `mfderivWithin`	—	`Nat.instAtLeastTwoHAddOfNat` `IsManifold.instOfNatWithTopENat_1` `RingHomInvPair.ids` `mlieBracketWithin_swap` `Pi.neg_apply` `mlieBracketWithin_smul_right` `smul_neg` `neg_add_rev` `neg_neg` `neg_smul` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.const_add_termg` `add_zero`
`mlieBracketWithin_smul_right` 📖	mathematical	`MDifferentiableWithinAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `modelWithCornersSelf` `chartedSpaceSelf` `Prod.normedAddCommGroup` `Prod.normedSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `IsManifold.instOfNatWithTopENat_1` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `UniqueMDiffWithinAt`	`mlieBracketWithin` `Pi.smul'` `TangentSpace` `SMulZeroClass.toSMul` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupTangentSpace` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `instModuleTangentSpace` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddZero.toZero` `AddZeroClass.toAddZero` `ENormedAddMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toENormedAddMonoid` `DFunLike.coe` `ContinuousLinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NormedField.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `NormedSpace.toModule` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `NormedSpace.fromTangentSpace` `ContinuousLinearMap` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ContinuousLinearMap.funLike` `mfderivWithin`	—	`Nat.instAtLeastTwoHAddOfNat` `IsManifold.instOfNatWithTopENat_1` `RingHomInvPair.ids` `mpullbackWithin_smul` `lieBracketWithin_smul_right` `MDifferentiableWithinAt.differentiableWithinAt_comp_extChartAt_symm` `MDifferentiableWithinAt.differentiableWithinAt_mpullbackWithin_vectorField` `Pi.add_def` `mpullback_add_apply` `mpullback_mfderivWithin_apply_smul` `mpullback_smul` `ModelWithCorners.left_inv` `OpenPartialHomeomorph.left_inv`
`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.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `IsManifold.instOfNatWithTopENat_1` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `Bundle.TotalSpace.mk'`	`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.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `IsManifold.instOfNatWithTopENat_1` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `Bundle.TotalSpace.mk'`	`mlieBracket` `Pi.instAdd` `TangentSpace` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `instTopologicalSpaceTangentSpace` `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.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `IsManifold.instOfNatWithTopENat_1` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `Bundle.TotalSpace.mk'`	`mlieBracket` `Pi.instAdd` `TangentSpace` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `instTopologicalSpaceTangentSpace` `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.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `IsManifold.instOfNatWithTopENat_1` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `Bundle.TotalSpace.mk'`	`mlieBracket` `Pi.instSMul` `TangentSpace` `SMulZeroClass.toSMul` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupTangentSpace` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `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.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `IsManifold.instOfNatWithTopENat_1` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `Bundle.TotalSpace.mk'`	`mlieBracket` `Pi.instSMul` `TangentSpace` `SMulZeroClass.toSMul` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupTangentSpace` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `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_smul_left` 📖	mathematical	`MDifferentiableAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `modelWithCornersSelf` `chartedSpaceSelf` `Prod.normedAddCommGroup` `Prod.normedSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `IsManifold.instOfNatWithTopENat_1` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle`	`mlieBracket` `Pi.smul'` `TangentSpace` `SMulZeroClass.toSMul` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupTangentSpace` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `instModuleTangentSpace` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddZero.toZero` `AddZeroClass.toAddZero` `ENormedAddMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toENormedAddMonoid` `NegZeroClass.toNeg` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DFunLike.coe` `ContinuousLinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NormedField.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `NormedSpace.toModule` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `NormedSpace.fromTangentSpace` `ContinuousLinearMap` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ContinuousLinearMap.funLike` `mfderiv`	—	`Nat.instAtLeastTwoHAddOfNat` `IsManifold.instOfNatWithTopENat_1` `RingHomInvPair.ids` `mlieBracketWithin_univ` `mfderivWithin_univ` `mlieBracketWithin_smul_left` `mdifferentiableWithinAt_univ` `uniqueMDiffWithinAt_univ`
`mlieBracket_smul_right` 📖	mathematical	`MDifferentiableAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `modelWithCornersSelf` `chartedSpaceSelf` `Prod.normedAddCommGroup` `Prod.normedSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `IsManifold.instOfNatWithTopENat_1` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle`	`mlieBracket` `Pi.smul'` `TangentSpace` `SMulZeroClass.toSMul` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupTangentSpace` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `instModuleTangentSpace` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddZero.toZero` `AddZeroClass.toAddZero` `ENormedAddMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toENormedAddMonoid` `DFunLike.coe` `ContinuousLinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NormedField.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `NormedSpace.toModule` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `NormedSpace.fromTangentSpace` `ContinuousLinearMap` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `ContinuousLinearMap.funLike` `mfderiv`	—	`Nat.instAtLeastTwoHAddOfNat` `IsManifold.instOfNatWithTopENat_1` `RingHomInvPair.ids` `mlieBracketWithin_univ` `mfderivWithin_univ` `mlieBracketWithin_smul_right` `mdifferentiableWithinAt_univ` `uniqueMDiffWithinAt_univ`
`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.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `instIsManifoldOfNatWithTopENatOfMinSmoothness_1` `instIsManifoldMinSmoothnessOfNatWithTopENat_1` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `Bundle.TotalSpace.mk'` `UniqueMDiffOn` `ContMDiffWithinAt` `Set` `Set.instMembership` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `instPreorderENat` `minSmoothness` `instOfNatAtLeastTwo` `WithTop.natCast` `ENat.instNatCast` `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.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `instIsManifoldOfNatWithTopENatOfMinSmoothness_1` `instIsManifoldMinSmoothnessOfNatWithTopENat_1` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `Bundle.TotalSpace.mk'` `UniqueMDiffOn` `ContMDiffWithinAt` `Set` `Set.instMembership` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `instPreorderENat` `minSmoothness` `instOfNatAtLeastTwo` `WithTop.natCast` `ENat.instNatCast` `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.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `IsManifold.instOfNatWithTopENat_1` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `Bundle.TotalSpace.mk'` `UniqueMDiffOn` `ContMDiffWithinAt` `WithTop` `ENat` `instOfNatAtLeastTwo` `WithTop.natCast` `ENat.instNatCast` `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_mfderivWithin_apply_smul` 📖	mathematical	`MDifferentiableWithinAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `modelWithCornersSelf` `chartedSpaceSelf`	`mpullback` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `PartialEquiv.toFun` `extChartAt` `TangentSpace` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `instTopologicalSpaceTangentSpace` `ENormedAddMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toENormedAddMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `instModuleTangentSpace` `DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `ContinuousLinearMap.funLike` `fderivWithin` `PartialEquiv.symm` `Set` `Set.instInter` `Set.preimage` `Set.range` `ModelWithCorners.toFun'` `mpullbackWithin` `AddCommMonoid.toAddMonoid` `SMulWithZero.toSMulZeroClass` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `MulActionWithZero.toSMulWithZero` `Module.toMulActionWithZero` `mfderivWithin`	—	`Nat.instAtLeastTwoHAddOfNat` `RingHomCompTriple.ids` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `extChartAt_to_inv` `mfderivWithin_extChartAt_symm_inverse_apply` `IsManifold.instOfNatWithTopENat_1`
`mpullback_mlieBracket` 📖	mathematical	`MDifferentiableAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `instIsManifoldOfNatWithTopENatOfMinSmoothness_1` `instIsManifoldMinSmoothnessOfNatWithTopENat_1` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `Bundle.TotalSpace.mk'` `ContMDiffAt` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `instPreorderENat` `minSmoothness` `instOfNatAtLeastTwo` `WithTop.natCast` `ENat.instNatCast` `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.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `instIsManifoldOfNatWithTopENatOfMinSmoothness_1` `instIsManifoldMinSmoothnessOfNatWithTopENat_1` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `Bundle.TotalSpace.mk'` `UniqueMDiffOn` `ContMDiffAt` `Set` `Set.instMembership` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `instPreorderENat` `minSmoothness` `instOfNatAtLeastTwo` `WithTop.natCast` `ENat.instNatCast` `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` `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