Basic

📁 Source: Mathlib/Geometry/Manifold/IsManifold/Basic.lean

Statistics

Metric	Count
Definitions LEInfty, IsManifold, maximalAtlas, «term𝓘(_)»»), «term𝓘(_,_)»»), ModelWithCorners, Boundaryless, apply, symm_apply, instCoeFunForall, ofConvexRange, ofTargetUniv, of_convex_range, of_target_univ, pi, prod, tangent, toFun', toHomeomorph, toPartialEquiv, TangentBundle, TangentSpace, contDiffGroupoid, contDiffPregroupoid, instAddCommGroupTangentSpace, instContinuousConstSMulTangentSpace, instContinuousSMulTangentSpace, instInhabitedTangentSpace, instIsTopologicalAddGroupTangentSpace, instModuleTangentSpace, instPathConnectedSpaceTangentSpaceReal, instTopologicalSpaceTangentSpace, modelWithCornersSelf	33
Theorems mem_of_source_eq_empty, mem_of_source_eq_empty, convex_isRCLikeNormedField, out, chart_mem_maximalAtlas, compatible_of_mem_maximalAtlas, disjointUnion, empty, instLEInftyCastWithTopENat, instLEInftyOfNatWithTopENat, instLEInftyOfNatWithTopENat_1, instLEInftyOfNatWithTopENat_2, instLEInftySomeENat, instOfNatWithTopENat, instOfNatWithTopENat_1, instOfNatWithTopENat_2, instOfSomeENatTopOfLEInfty, instOfTopWithTopENat, maximalAtlas_subset_of_le, mem_maximalAtlas_iff, mem_maximalAtlas_prod, mk', of_discreteTopology, of_le, prod, subset_maximalAtlas, toHasGroupoid, range_eq_univ, continuous, continuousAt, continuousAt_symm, continuousOn_symm, continuousWithinAt, continuousWithinAt_symm, continuous_invFun, continuous_symm, continuous_toFun, convex_range, convex_range', ext, ext_iff, image_eq, image_mem_nhdsWithin, injective, isClosedEmbedding, isClosed_range, leftInverse, left_inv, locallyCompactSpace, map_nhdsWithin_eq, map_nhds_eq, mk_coe, mk_symm, nonempty_interior, nonempty_interior', preimage_image, prod_apply, prod_source, prod_symm_apply, prod_target, range_eq_closure_interior, range_eq_target, range_eq_univ, range_eq_univ_of_not_isRCLikeNormedField, range_eq_univ_prod, range_prod, range_subset_closure_interior, rightInvOn, right_inv, secondCountableTopology, source_eq, symm_comp_self, symm_continuousWithinAt_comp_right_iff, symm_map_nhdsWithin_image, symm_map_nhdsWithin_range, t1Space, target_eq, toHomeomorph_apply, toHomeomorph_symm_apply, toPartialEquiv_coe, toPartialEquiv_coe_symm, uniqueDiffOn, uniqueDiffOn_preimage, uniqueDiffOn_preimage_source, uniqueDiffWithinAt_image, isManifold_singleton, invFun, instIsManifoldSubtypeMem, isManifold_singleton, contDiffGroupoid_le, contDiffGroupoid_prod, contDiffGroupoid_zero_eq, instClosedUnderRestrictionContDiffGroupoid, instIsManifoldModelSpace, isManifold_of_contDiffOn, modelWithCornersSelf_boundaryless, modelWithCornersSelf_coe, modelWithCornersSelf_coe_symm, modelWithCornersSelf_partialEquiv, modelWithCornersSelf_prod, modelWithCorners_prod_coe, modelWithCorners_prod_coe_symm, modelWithCorners_prod_toPartialEquiv, ofSet_mem_contDiffGroupoid, symm_trans_mem_contDiffGroupoid	105
Total	138

ContDiffGroupoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_of_source_eq_empty 📖	mathematical	PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv Set Set.instEmptyCollection	OpenPartialHomeomorph StructureGroupoid instMembershipOpenPartialHomeomorphStructureGroupoid contDiffGroupoid	—	Set.mem_preimage OpenPartialHomeomorph.image_source_eq_target Set.image_empty

ContinuousGroupoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_of_source_eq_empty 📖	mathematical	PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv Set Set.instEmptyCollection	OpenPartialHomeomorph StructureGroupoid instMembershipOpenPartialHomeomorphStructureGroupoid continuousGroupoid	—	contDiffGroupoid_zero_eq ContDiffGroupoid.mem_of_source_eq_empty

Convex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
convex_isRCLikeNormedField 📖	mathematical	Convex Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField	NormedSpace.restrictScalars DenselyNormedField.toNormedField RCLike.toDenselyNormedField IsRCLikeNormedField.rclike NontriviallyNormedField.toNormedField RCLike.toNormedAlgebra	—	algebraMap_smul Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace

ENat

Definitions

Name	Category	Theorems
LEInfty 📖	CompData	5 math math: IsManifold.instLEInftyOfNatWithTopENat_2, IsManifold.instLEInftyOfNatWithTopENat, IsManifold.instLEInftyOfNatWithTopENat_1, IsManifold.instLEInftySomeENat, IsManifold.instLEInftyCastWithTopENat

ENat.LEInfty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
out 📖	mathematical	—	WithTop ENat Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat WithTop.some Top.top instTopENat	—	—

IsManifold

Definitions

Name	Category	Theorems
maximalAtlas 📖	CompOp	12 math math: mem_maximalAtlas_iff, Manifold.IsImmersionAt.codChart_mem_maximalAtlas, chart_mem_maximalAtlas, Manifold.LocalPresentationAt.domChart_mem_maximalAtlas, Manifold.IsImmersionAtOfComplement.domChart_mem_maximalAtlas, Manifold.LiftSourceTargetPropertyAt.domChart_mem_maximalAtlas, Manifold.LiftSourceTargetPropertyAt.codChart_mem_maximalAtlas, maximalAtlas_subset_of_le, Manifold.IsImmersionAt.domChart_mem_maximalAtlas, subset_maximalAtlas, Manifold.IsImmersionAtOfComplement.codChart_mem_maximalAtlas, Manifold.LocalPresentationAt.codChart_mem_maximalAtlas

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
chart_mem_maximalAtlas 📖	mathematical	—	OpenPartialHomeomorph Set Set.instMembership maximalAtlas chartAt	—	StructureGroupoid.chart_mem_maximalAtlas toHasGroupoid
compatible_of_mem_maximalAtlas 📖	mathematical	OpenPartialHomeomorph Set Set.instMembership maximalAtlas	StructureGroupoid instMembershipOpenPartialHomeomorphStructureGroupoid contDiffGroupoid OpenPartialHomeomorph.trans OpenPartialHomeomorph.symm	—	StructureGroupoid.compatible_of_mem_maximalAtlas
disjointUnion 📖	mathematical	—	IsManifold instTopologicalSpaceSum ChartedSpace.sum	—	isEmpty_or_nonempty ContDiffGroupoid.mem_of_source_eq_empty Set.eq_empty_of_isEmpty instIsEmptySubtype Topology.IsOpenEmbedding.inl Topology.IsOpenEmbedding.inr ChartedSpace.mem_atlas_sum OpenPartialHomeomorph.lift_openEmbedding_trans HasGroupoid.compatible toHasGroupoid Set.ext
empty 📖	mathematical	—	IsManifold	—	isManifold_of_contDiffOn OpenPartialHomeomorph.trans_source Set.eq_empty_of_isEmpty instIsEmptySubtype Set.preimage_empty Set.inter_empty Subtype.preimage_val_eq_preimage_val_iff Set.empty_inter
instLEInftyCastWithTopENat 📖	mathematical	—	ENat.LEInfty WithTop ENat AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	le_top
instLEInftyOfNatWithTopENat 📖	mathematical	—	ENat.LEInfty	—	instLEInftyCastWithTopENat
instLEInftyOfNatWithTopENat_1 📖	mathematical	—	ENat.LEInfty WithTop ENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	instLEInftyCastWithTopENat
instLEInftyOfNatWithTopENat_2 📖	mathematical	—	ENat.LEInfty WithTop ENat WithTop.zero instZeroENat	—	instLEInftyCastWithTopENat
instLEInftySomeENat 📖	mathematical	—	ENat.LEInfty WithTop.some ENat	—	le_top
instOfNatWithTopENat 📖	mathematical	—	IsManifold WithTop ENat WithTop.zero instZeroENat	—	contDiffGroupoid_zero_eq mk'
instOfNatWithTopENat_1 📖	mathematical	—	IsManifold WithTop ENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	Nat.instAtLeastTwoHAddOfNat of_le one_le_two WithTop.zeroLEOneClass IsOrderedRing.toZeroLEOneClass WithTop.addLeftMono IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid
instOfNatWithTopENat_2 📖	mathematical	—	IsManifold WithTop ENat instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat of_le WithTop.addLeftMono IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid WithTop.zeroLEOneClass IsOrderedRing.toZeroLEOneClass WithTop.charZero
instOfSomeENatTopOfLEInfty 📖	mathematical	—	IsManifold	—	of_le ENat.LEInfty.out
instOfTopWithTopENat 📖	mathematical	—	IsManifold	—	of_le le_top
maximalAtlas_subset_of_le 📖	mathematical	WithTop ENat Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat	Set OpenPartialHomeomorph Set.instHasSubset maximalAtlas	—	StructureGroupoid.maximalAtlas_mono contDiffGroupoid_le
mem_maximalAtlas_iff 📖	mathematical	—	OpenPartialHomeomorph Set Set.instMembership maximalAtlas StructureGroupoid.maximalAtlas contDiffGroupoid	—	—
mem_maximalAtlas_prod 📖	mathematical	OpenPartialHomeomorph Set Set.instMembership maximalAtlas	instTopologicalSpaceProd ModelProd instTopologicalSpaceModelProd Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelWithCorners.prod prodChartedSpace OpenPartialHomeomorph.prod	—	OpenPartialHomeomorph.prod_symm_trans_prod contDiffGroupoid_prod
mk' 📖	mathematical	—	IsManifold	—	—
of_discreteTopology 📖	mathematical	—	IsManifold UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf ChartedSpace.of_discreteTopology	—	isManifold_of_contDiffOn ContDiff.contDiffOn contDiff_of_subsingleton Unique.instSubsingleton
of_le 📖	mathematical	WithTop ENat Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat	IsManifold	—	hasGroupoid_of_le toHasGroupoid contDiffGroupoid_le mk'
prod 📖	mathematical	—	IsManifold Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd ModelWithCorners.prod instTopologicalSpaceProd prodChartedSpace	—	OpenPartialHomeomorph.prod_symm OpenPartialHomeomorph.prod_trans StructureGroupoid.compatible toHasGroupoid contDiffGroupoid_prod
subset_maximalAtlas 📖	mathematical	—	Set OpenPartialHomeomorph Set.instHasSubset atlas maximalAtlas	—	StructureGroupoid.subset_maximalAtlas toHasGroupoid
toHasGroupoid 📖	mathematical	—	HasGroupoid contDiffGroupoid	—	—

Manifold

Definitions

Name	Category	Theorems
«term𝓘(_)» 📖» "API Documentation")	CompOp	—
«term𝓘(_,_)» 📖» "API Documentation")	CompOp	—

ModelWithCorners

Definitions

Name	Category	Theorems
Boundaryless 📖	CompData	2 math math: modelWithCornersSelf_boundaryless, range_eq_univ_prod
instCoeFunForall 📖	CompOp	—
ofConvexRange 📖	CompOp	—
ofTargetUniv 📖	CompOp	—
of_convex_range 📖	CompOp	—
of_target_univ 📖	CompOp	—
pi 📖	CompOp	—
prod 📖	CompOp	190 math math: contMDiff_prod_assoc, Prod.instLieGroup, Bundle.ContMDiffRiemannianMetric.contMDiff, Bundle.mdifferentiableAt_proj, Trivialization.mdifferentiableAt_section_iff, ContMDiffMul.prod, range_prod, Bundle.contMDiffOn_zeroSection, MDifferentiableAt.mfderiv_prod, mdifferentiableWithinAt_totalSpace, ContMDiffOn.prodMk, Manifold.IsImmersionOfComplement.prodMap, Trivialization.mdifferentiableOn_section_baseSet_iff, HasMFDerivWithinAt.prodMk, ContMDiffAdd.prod, ContMDiffMul.contMDiff_mul, Bundle.contMDiffWithinAt_zeroSection, mdifferentiableOn_snd, contMDiff_mul, contMDiffWithinAt_snd, contMDiffWithinAt_prod_iff, UniqueMDiffOn.prod, IsLocalFrameOn.contMDiffAt_of_coeff, contMDiff_equivTangentBundleProd_symm, mdifferentiableWithinAt_section, Trivialization.contMDiffAt_iff, Trivialization.contMDiffOn_symm_trans, Trivialization.contMDiff_iff, ContMDiffAdd.contMDiff_add, Manifold.IsSmoothEmbedding.prodMap, Trivialization.contMDiffOn_section_iff, Manifold.IsImmersionAtOfComplement.prodMap, Diffeomorph.coe_prodCongr, hasMFDerivAt_fst, writtenInExtChart_prod, Bundle.contMDiffAt_zeroSection, prod_target, MDifferentiable.prodMap, equivTangentBundleProd_apply, HasMFDerivWithinAt.prodMap, mdifferentiableAt_fst, MDifferentiableOn.prodMk, MDifferentiableAt.prodMap', ContMDiffAt.prodMap, mdifferentiableAt_totalSpace, mdifferentiableOn_fst, MDifferentiableAt.prodMk, Diffeomorph.prodCongr_symm, Trivialization.mdifferentiableAt_totalSpace_iff, mdifferentiableAt_hom_bundle, IsLocalFrameOn.mdifferentiableAt_of_coeff_aux, mdifferentiable_fst, modelWithCorners_prod_coe, Bundle.TotalSpace.isManifold, mdifferentiableAt_snd, mfderiv_prodMap, UniqueMDiffWithinAt.bundle_preimage', IsContMDiffRiemannianBundle.exists_contMDiff, prod_symm_apply, contMDiff_snd, contMDiffAt_prod_iff, tangentMap_prodSnd, HasMFDerivAt.prodMap, IsLocalFrameOn.mdifferentiableOn_of_coeff, prod_source, hasMFDerivWithinAt_fst, MDifferentiableOn.prodMap, Trivialization.contMDiffOn_localFrame_baseSet, modelWithCorners_prod_coe_symm, contMDiff_smul, Bundle.mdifferentiableWithinAt_proj, IsLocalFrameOn.contMDiffOn, MDifferentiableWithinAt.prodMk, Bundle.contMDiffWithinAt_totalSpace, Diffeomorph.coe_prodComm, Bundle.mdifferentiableOn_proj, equivTangentBundleProd_symm_apply_snd, IsLocalFrameOn.contMDiffAt, contMDiffAt_hom_bundle, ContMDiffOn.prodMap, ContMDiffRing.contMDiff_mul, contMDiff_prod_iff, FiberBundle.extChartAt, mfderiv_prod_right, Bundle.contMDiffWithinAt_proj, boundary_of_boundaryless_left, modelWithCornersSelf_prod, Bundle.contMDiffAt_totalSpace, Trivialization.contMDiffOn_section_baseSet_iff, mdifferentiable_snd, mdifferentiableAt_prod_iff, MDifferentiable.prodMk, OpenPartialHomeomorph.extend_prod, contMDiffWithinAt_fst, Bundle.contMDiffOn_proj, ContMDiffWithinAt.prodMk, Bundle.contMDiff_proj, contMDiffOn_fst, contMDiffOn_prod_iff, contMDiffAt_section_of_mem_baseSet, Manifold.IsImmersionAt.prodMap, IsManifold.prod, mfderivWithin_prodMap, UniqueMDiffWithinAt.bundle_preimage, Manifold.IsImmersion.prodMap, Bundle.mdifferentiableWithinAt_zeroSection, mfderiv_snd, modelWithCorners_prod_toPartialEquiv, Trivialization.mdifferentiableWithinAt_section_iff, Bundle.contMDiff_zeroSection, FiberBundle.extChartAt_target, contMDiffAt_localFrame_of_mem, mdifferentiableWithinAt_snd, mfderiv_prodMk, hasMFDerivWithinAt_snd, mdifferentiableAt_section, Bundle.mdifferentiable_proj, boundary_of_boundaryless_right, range_eq_univ_prod, prod_apply, ContMDiffSection.contMDiff, IsManifold.mem_maximalAtlas_prod, contMDiff_equivTangentBundleProd, Trivialization.contMDiffWithinAt_iff, UniqueMDiffOn.bundle_preimage, Bundle.contMDiffAt_section, boundary_prod, equivTangentBundleProd_eq_tangentMap_prod_tangentMap, mdifferentiable_prod_iff, mdifferentiableOn_prod_iff, mfderivWithin_prodMk, Trivialization.mdifferentiableOn_section_iff, ContMDiffAt.prodMap', tangentMap_prodFst, ContMDiffWithinAt.prodMap', mdifferentiableWithinAt_fst, Trivialization.contMDiffAt_section_iff, IsLocalFrameOn.contMDiffOn_of_coeff, BoundarylessManifold.prod, contMDiff_add, Diffeomorph.prodComm_symm, Prod.instLieAddGroup, HasMFDerivAt.prodMk, Trivialization.contMDiffOn_symm, ContMDiffAt.prodMk, Bundle.contMDiffAt_proj, Trivialization.contMDiffOn_iff, contMDiff_tangentBundleModelSpaceHomeomorph, hasMFDerivAt_snd, MDifferentiableWithinAt.prodMap, Bundle.contMDiffWithinAt_section, Bundle.mdifferentiableOn_zeroSection, Trivialization.mdifferentiableWithinAt_totalSpace_iff, ContMDiffSection.mdifferentiable', contMDiff_tangentBundleModelSpaceHomeomorph_symm, mfderiv_fst, ContMDiffSection.mdifferentiableAt, UniqueMDiffWithinAt.prod, equivTangentBundleProd_symm_apply_proj, ContMDiffSection.mdifferentiable, ContMDiffWithinAt.prodMap, Bundle.mdifferentiable_zeroSection, contMDiffAt_fst, mdifferentiableWithinAt_prod_iff, IsLocalFrameOn.mdifferentiableAt_of_coeff, tangentMap_prod_right, tangentMap_prod_left, ContMDiffSection.contMDiff_toFun, contDiffGroupoid_prod, interior_prod, contMDiffOn_snd, mfderiv_prod_left, MDifferentiableWithinAt.prodMap', mdifferentiableWithinAt_hom_bundle, IsLocalFrameOn.contMDiffAt_of_coeff_aux, Trivialization.contMDiffOn, contMDiffOn_section_of_mem_baseSet₀, contMDiff_fst, Bundle.mdifferentiableAt_zeroSection, boundary_product, MDifferentiableAt.prodMap, Trivialization.mdifferentiable, ContMDiff.prodMap, contMDiffWithinAt_hom_bundle, contMDiffAt_snd, Trivialization.contMDiffWithinAt_section, extChartAt_prod, Manifold.LiftSourceTargetPropertyAt.prodMap, contMDiffOn_section_of_mem_baseSet, ContMDiff.prodMk
tangent 📖	CompOp	21 math math: TangentBundle.tangentMap_tangentBundle_pure, contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt, contMDiff_addInvariantVectorField, contMDiff_mulInvariantVectorField, contMDiff_equivTangentBundleProd_symm, contMDiffAt_mulInvariantVectorField, mdifferentiableAt_addInvariantVectorField, ContMDiff.contMDiff_tangentMap, mdifferentiable_mulInvariantVectorField, contMDiff_vectorSpace_iff_contDiff, UniqueMDiffOn.tangentBundle_proj_preimage, contMDiffAt_vectorSpace_iff_contDiffAt, mdifferentiable_addInvariantVectorField, contMDiff_equivTangentBundleProd, mdifferentiableAt_mulInvariantVectorField, ContMDiffOn.contMDiffOn_tangentMapWithin, contMDiffAt_addInvariantVectorField, contMDiff_tangentBundleModelSpaceHomeomorph, contMDiff_tangentBundleModelSpaceHomeomorph_symm, contMDiffOn_vectorSpace_iff_contDiffOn, contMDiff_snd_tangentBundle_modelSpace
toFun' 📖	CompOp	182 math math: contMDiffAt_iff_of_mem_source, OpenPartialHomeomorph.extend_preimage_inter_eq, range_prod, preimage_image, SmoothBumpFunction.support_eq_symm_image, MDifferentiableWithinAt.differentiableWithinAt_mpullbackWithin_vectorField, mdifferentiableWithinAt_iff_of_mem_maximalAtlas, injective, symm_continuousWithinAt_comp_right_iff, contMDiffAt_iff_source, eventually_enorm_mfderivWithin_symm_extChartAt_lt, extChartAt_target_eventuallyEq, TangentBundle.symmL_trivializationAt, ContinuousWithinAt.extChartAt_symm_preimage_inter_range_eventuallyEq, map_extChartAt_symm_nhdsWithin, mdifferentiableOn_symm, tangentCoordChange_def, image_eq, map_extChartAt_symm_nhdsWithin', OpenPartialHomeomorph.extend_target_mem_nhdsWithin, map_extChartAt_symm_nhdsWithin_range', extChartAt_preimage_inter_eq, map_extChartAt_symm_nhdsWithin_range, map_extChartAt_nhdsWithin', inTangentCoordinates_eq_mfderiv_comp, mdifferentiableAt_iff, MDifferentiableWithinAt.differentiableWithinAt_writtenInExtChartAt, extChartAt_preimage_mem_nhdsWithin', uniqueDiffOn_preimage, hasMFDerivAt, extChartAt_target_mem_nhdsWithin, eventually_norm_mfderivWithin_symm_extChartAt_lt, extChartAt_self_apply, extChartAt_target_union_compl_range_mem_nhds_of_mem, mapsTo_extChartAt, symm_comp_self, preimage_extChartAt_eventuallyEq_compl_singleton, contMDiff_model, OpenPartialHomeomorph.extend_image_target_mem_nhds, contMDiffAt_iff_source_of_mem_source, extChartAt_target_mem_nhdsWithin_of_mem, SmoothBumpFunction.tsupport_subset_symm_image_closedBall, MDifferentiableAt.differentiableWithinAt_writtenInExtChartAt, TangentBundle.trivializationAt_apply, map_nhdsWithin_eq, modelWithCorners_prod_coe, frontier_range_modelWithCornersEuclideanHalfSpace, OpenPartialHomeomorph.continuousWithinAt_writtenInExtend_iff, OpenPartialHomeomorph.map_extend_symm_nhdsWithin, mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm, range_eq_univ_of_not_isRCLikeNormedField, toPartialEquiv_coe, OpenPartialHomeomorph.extend_target, extChartAt_self_eq, OpenPartialHomeomorph.contDiffWithinAt_extend_coord_change', contDiffWithinAtProp_self_source, OpenPartialHomeomorph.extend_coord_change_source_mem_nhdsWithin', SmoothBumpFunction.ball_subset, OpenPartialHomeomorph.extend_coord_change_source_mem_nhdsWithin, VectorField.mlieBracketWithin_def, contMDiffAt_iff, OpenPartialHomeomorph.map_extend_nhds, extChartAt_preimage_mem_nhdsWithin, symm_map_nhdsWithin_range, extChartAt_target_mem_nhdsWithin', contMDiffWithinAt_extChartAt_symm_range_self, continuousWithinAt, OpenPartialHomeomorph.extend_symm_preimage_inter_range_eventuallyEq_aux, contMDiffWithinAt_iff_source_of_mem_maximalAtlas, ext_coord_change_source, leftInverse, mdifferentiableAt, nonempty_interior, MDifferentiableAt.mfderiv, hasFDerivWithinAt_tangentCoordChange, ContinuousWithinAt.nhdsWithin_extChartAt_symm_preimage_inter_range, differentiableWithinAtProp_self_source, MDifferentiableWithinAt.mfderivWithin, contMDiffWithinAt_iff, OpenPartialHomeomorph.contDiffWithinAt_extend_coord_change, map_nhds_eq, extChartAt_target_eventuallyEq', hasMFDerivWithinAt, tangentBundleCore_coordChange, modelWithCornersEuclideanHalfSpace_zero, contDiffOn_fderiv_coord_change, SmoothBumpFunction.isClosed_symm_image_closedBall, image_mem_nhdsWithin, extChartAt_target_subset_range, map_extChartAt_nhds', mdifferentiableWithinAt_iff', OpenPartialHomeomorph.extend_target_eventuallyEq, target_eq, OpenPartialHomeomorph.extend_target', convex_range, contDiffWithinAtProp_self_target, VectorField.eventuallyEq_mpullback_mpullbackWithin_extChartAt, map_extChartAt_nhdsWithin, uniqueMDiffOn, IccRightChart_extend_top_mem_frontier, continuousAt, continuous, symm_map_nhdsWithin_image, uniqueMDiffWithinAt_iff_inter_range, nhdsWithin_extChartAt_target_eq_of_mem, VectorField.contMDiffWithinAt_mpullbackWithin_extChartAt_symm, mdifferentiableWithinAt_iff_source_of_mem_maximalAtlas, mdifferentiableWithinAt_iff, mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm', OpenPartialHomeomorph.interior_extend_target_subset_interior_range, writtenInExtChartAt_sumSwap_eventuallyEq_id, interior_range_modelWithCornersEuclideanHalfSpace, mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt', OpenPartialHomeomorph.extend_coe, OpenPartialHomeomorph.extend_symm_continuousWithinAt_comp_right_iff, mdifferentiable, range_eq_closure_interior, range_subset_closure_interior, prod_apply, transContinuousLinearEquiv_range, OpenPartialHomeomorph.map_extend_nhdsWithin, mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt, contMDiffWithinAt_iff_source, OpenPartialHomeomorph.nhdsWithin_extend_target_eq, nhdsWithin_extChartAt_target_eq, contMDiffWithinAt_iff_source_of_mem_source, contMDiffWithinAt_iff_of_mem_maximalAtlas, mdifferentiableAt_iff_source_of_mem_source, mk_coe, mdifferentiableAt_iff_of_mem_source, uniqueDiffWithinAt_image, mdifferentiableWithinAt_extChartAt_symm, mdifferentiableOn, contMDiffWithinAt_extChartAt_symm_range, contDiffWithinAt_ext_coord_change, eventually_norm_mfderivWithin_symm_extChartAt_comp_lt, OpenPartialHomeomorph.extend_preimage_mem_nhdsWithin, contMDiffOn_extend_symm, toHomeomorph_apply, extChartAt_target, mdifferentiableWithinAt_iff_source_of_mem_source, isClosed_range, modelWithCornersSelf_coe, coe_transContinuousLinearEquiv, isClosedEmbedding, range_modelWithCornersEuclideanHalfSpace, OpenPartialHomeomorph.extend_target_subset_range, contMDiffOn_model_symm, mdifferentiableWithinAt_iff_of_mem_source, OpenPartialHomeomorph.map_extend_symm_nhdsWithin_range, isInvertible_mfderivWithin_extChartAt_symm, VectorField.mlieBracketWithin_apply, VectorField.eventually_contMDiffWithinAt_mpullbackWithin_extChartAt_symm, uniqueDiffOn_preimage_source, SmoothBumpFunction.nhdsWithin_range_basis, extChartAt_target_eventuallyEq_of_mem, OpenPartialHomeomorph.extend_coord_change_source, rightInvOn, writtenInExtChartAt_sumInr_eventuallyEq_id, range_mem_nhds_isInteriorPoint, left_inv, OpenPartialHomeomorph.extend_symm_preimage_inter_range_eventuallyEq, isBoundaryPoint_iff, OpenPartialHomeomorph.mapsTo_extend, range_eq_univ, extChartAt_coe, writtenInExtChartAt_sumInl_eventuallyEq_id, UniqueMDiffOn.uniqueDiffWithinAt_range_inter, writtenInExtChartAt_comp, map_extChartAt_nhds, IccLeftChart_extend_bot_mem_frontier, uniqueDiffOn, differentiableWithinAtProp_self_target, contMDiffWithinAt_iff_of_mem_source, nhdsWithin_extChartAt_target_eq', Boundaryless.range_eq_univ, SmoothBumpFunction.image_eq_inter_preimage_of_subset_support, SmoothBumpFunction.closedBall_subset, tangentBundleCore_coordChange_achart, SmoothBumpFunction.isCompact_symm_image_closedBall, mdifferentiableWithinAt, SmoothBumpFunction.ball_inter_range_eq_ball_inter_target
toHomeomorph 📖	CompOp	2 math math: toHomeomorph_apply, toHomeomorph_symm_apply
toPartialEquiv 📖	CompOp	14 math math: continuous_invFun, prod_target, source_eq, ext_iff, toPartialEquiv_coe, prod_source, range_eq_target, target_eq, continuous_toFun, modelWithCorners_prod_toPartialEquiv, convex_range', modelWithCornersSelf_partialEquiv, nonempty_interior', toPartialEquiv_coe_symm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous 📖	mathematical	—	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toFun'	—	continuous_toFun
continuousAt 📖	mathematical	—	ContinuousAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toFun'	—	Continuous.continuousAt continuous
continuousAt_symm 📖	mathematical	—	ContinuousAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup PartialEquiv.toFun symm	—	Continuous.continuousAt continuous_symm
continuousOn_symm 📖	mathematical	—	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup PartialEquiv.toFun symm	—	Continuous.continuousOn continuous_symm
continuousWithinAt 📖	mathematical	—	ContinuousWithinAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toFun'	—	ContinuousAt.continuousWithinAt continuousAt
continuousWithinAt_symm 📖	mathematical	—	ContinuousWithinAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup PartialEquiv.toFun symm	—	Continuous.continuousWithinAt continuous_symm
continuous_invFun 📖	mathematical	—	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup PartialEquiv.invFun toPartialEquiv	—	—
continuous_symm 📖	mathematical	—	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup PartialEquiv.toFun symm	—	continuous_invFun
continuous_toFun 📖	mathematical	—	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup PartialEquiv.toFun toPartialEquiv	—	—
convex_range 📖	mathematical	—	Convex Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField Set.range toFun'	—	convex_range' algebraMap_smul Real.isScalarTower IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace range_eq_univ_of_not_isRCLikeNormedField
convex_range' 📖	mathematical	—	IsRCLikeNormedField NontriviallyNormedField.toNormedField Convex Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField NormedSpace.restrictScalars DenselyNormedField.toNormedField RCLike.toDenselyNormedField IsRCLikeNormedField.rclike RCLike.toNormedAlgebra Set.range PartialEquiv.toFun toPartialEquiv Set Set.univ	—	—
ext 📖	—	PartialEquiv.toFun toPartialEquiv PartialEquiv.invFun PartialEquiv.source PartialEquiv.target	—	—	—
ext_iff 📖	mathematical	—	PartialEquiv.toFun toPartialEquiv PartialEquiv.invFun PartialEquiv.source PartialEquiv.target	—	ext
image_eq 📖	mathematical	—	Set.image toFun' Set Set.instInter Set.preimage PartialEquiv.toFun symm Set.range	—	PartialEquiv.image_eq_target_inter_inv_preimage source_eq Set.subset_univ Set.inter_comm target_eq toPartialEquiv_coe_symm
image_mem_nhdsWithin 📖	mathematical	Set Filter Filter.instMembership nhds	nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toFun' Set.range Set.image	—	Filter.image_mem_map map_nhds_eq
injective 📖	mathematical	—	toFun'	—	leftInverse
isClosedEmbedding 📖	mathematical	—	Topology.IsClosedEmbedding UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toFun'	—	Function.LeftInverse.isClosedEmbedding TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace leftInverse continuous_symm continuous
isClosed_range 📖	mathematical	—	IsClosed UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.range toFun'	—	Topology.IsClosedEmbedding.isClosed_range isClosedEmbedding
leftInverse 📖	mathematical	—	PartialEquiv.toFun symm toFun'	—	left_inv
left_inv 📖	mathematical	—	PartialEquiv.toFun symm toFun'	—	PartialEquiv.left_inv' source_eq
locallyCompactSpace 📖	mathematical	—	LocallyCompactSpace	—	symm_map_nhdsWithin_range Filter.HasBasis.map Filter.HasBasis.inf_principal compact_basis_nhds LocallyCompactSpace.of_hasBasis IsCompact.image IsCompact.inter_right isClosed_range continuous_symm
map_nhdsWithin_eq 📖	mathematical	—	Filter.map toFun' nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.image	—	Topology.IsEmbedding.map_nhdsWithin_eq Topology.IsClosedEmbedding.isEmbedding isClosedEmbedding
map_nhds_eq 📖	mathematical	—	Filter.map toFun' nhds nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.range	—	Topology.IsEmbedding.map_nhds_eq Topology.IsClosedEmbedding.isEmbedding isClosedEmbedding
mk_coe 📖	mathematical	PartialEquiv.source Set.univ IsRCLikeNormedField NontriviallyNormedField.toNormedField Convex Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField NormedSpace.restrictScalars DenselyNormedField.toNormedField RCLike.toDenselyNormedField IsRCLikeNormedField.rclike RCLike.toNormedAlgebra Set.range PartialEquiv.toFun Set Set.Nonempty interior Continuous PartialEquiv.invFun	toFun'	—	—
mk_symm 📖	mathematical	PartialEquiv.source Set.univ IsRCLikeNormedField NontriviallyNormedField.toNormedField Convex Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField NormedSpace.restrictScalars DenselyNormedField.toNormedField RCLike.toDenselyNormedField IsRCLikeNormedField.rclike RCLike.toNormedAlgebra Set.range PartialEquiv.toFun Set Set.Nonempty interior Continuous PartialEquiv.invFun	symm PartialEquiv.symm	—	—
nonempty_interior 📖	mathematical	—	Set.Nonempty interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.range toFun'	—	nonempty_interior'
nonempty_interior' 📖	mathematical	—	Set.Nonempty interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.range PartialEquiv.toFun toPartialEquiv	—	—
preimage_image 📖	mathematical	—	Set.preimage toFun' Set.image	—	Function.Injective.preimage_image injective
prod_apply 📖	mathematical	—	toFun' Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd prod	—	—
prod_source 📖	mathematical	—	PartialEquiv.source ModelProd toPartialEquiv Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup instTopologicalSpaceModelProd prod setOf Set Set.instMembership	—	—
prod_symm_apply 📖	mathematical	—	PartialEquiv.toFun ModelProd symm Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup instTopologicalSpaceModelProd prod	—	—
prod_target 📖	mathematical	—	PartialEquiv.target ModelProd toPartialEquiv Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup instTopologicalSpaceModelProd prod PartialEquiv.prod	—	—
range_eq_closure_interior 📖	mathematical	—	Set.range toFun' closure UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup interior	—	Set.Subset.antisymm range_subset_closure_interior IsClosed.closure_interior_subset isClosed_range
range_eq_target 📖	mathematical	—	Set.range PartialEquiv.toFun toPartialEquiv PartialEquiv.target	—	PartialEquiv.image_source_eq_target source_eq Set.image_univ
range_eq_univ 📖	mathematical	—	Set.range toFun' Set.univ	—	Boundaryless.range_eq_univ
range_eq_univ_of_not_isRCLikeNormedField 📖	mathematical	IsRCLikeNormedField NontriviallyNormedField.toNormedField	Set.range toFun' Set.univ	—	convex_range'
range_eq_univ_prod 📖	mathematical	—	Boundaryless Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd prod	—	Set.prod_range_range_eq Boundaryless.range_eq_univ Set.univ_prod_univ
range_prod 📖	mathematical	—	Set.range ModelProd toFun' Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup instTopologicalSpaceModelProd prod SProd.sprod Set Set.instSProd	—	—
range_subset_closure_interior 📖	mathematical	—	Set Set.instHasSubset Set.range toFun' closure UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup interior	—	Convex.closure_interior_eq_closure_of_nonempty_interior Real.instIsStrictOrderedRing SeminormedAddCommGroup.toIsTopologicalAddGroup instOrderTopologyReal IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul convex_range nonempty_interior subset_closure range_eq_univ_of_not_isRCLikeNormedField interior_univ IsClosed.closure_eq Set.instReflSubset
rightInvOn 📖	mathematical	—	Set.RightInvOn PartialEquiv.toFun symm toFun' Set.range	—	Function.LeftInverse.rightInvOn_range leftInverse
right_inv 📖	mathematical	Set Set.instMembership Set.range toFun'	PartialEquiv.toFun symm	—	rightInvOn
secondCountableTopology 📖	mathematical	—	SecondCountableTopology	—	Topology.IsEmbedding.secondCountableTopology Topology.IsClosedEmbedding.isEmbedding isClosedEmbedding
source_eq 📖	mathematical	—	PartialEquiv.source toPartialEquiv Set.univ	—	—
symm_comp_self 📖	mathematical	—	PartialEquiv.toFun symm toFun'	—	Function.LeftInverse.comp_eq_id leftInverse
symm_continuousWithinAt_comp_right_iff 📖	mathematical	—	ContinuousWithinAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup PartialEquiv.toFun symm Set Set.instInter Set.preimage Set.range toFun'	—	ContinuousWithinAt.comp continuousWithinAt Set.mapsTo_preimage symm_comp_self Function.comp_assoc Set.inter_univ Set.preimage_range left_inv Set.preimage_preimage continuousWithinAt_symm Set.inter_subset_left
symm_map_nhdsWithin_image 📖	mathematical	—	Filter.map PartialEquiv.toFun symm nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toFun' Set.image	—	map_nhdsWithin_eq Filter.map_map symm_comp_self Filter.map_id
symm_map_nhdsWithin_range 📖	mathematical	—	Filter.map PartialEquiv.toFun symm nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toFun' Set.range nhds	—	map_nhds_eq Filter.map_map symm_comp_self Filter.map_id
t1Space 📖	mathematical	—	T1Space	—	Topology.IsEmbedding.t2Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Topology.IsClosedEmbedding.toIsEmbedding isClosedEmbedding ChartedSpace.t1Space T2Space.t1Space
target_eq 📖	mathematical	—	PartialEquiv.target toPartialEquiv Set.range toFun'	—	Set.image_univ source_eq PartialEquiv.image_source_eq_target
toHomeomorph_apply 📖	mathematical	—	DFunLike.coe Homeomorph UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup EquivLike.toFunLike Homeomorph.instEquivLike toHomeomorph toFun'	—	—
toHomeomorph_symm_apply 📖	mathematical	—	DFunLike.coe Homeomorph UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup EquivLike.toFunLike Homeomorph.instEquivLike Homeomorph.symm toHomeomorph PartialEquiv.toFun symm	—	—
toPartialEquiv_coe 📖	mathematical	—	PartialEquiv.toFun toPartialEquiv toFun'	—	—
toPartialEquiv_coe_symm 📖	mathematical	—	PartialEquiv.toFun PartialEquiv.symm toPartialEquiv symm	—	—
uniqueDiffOn 📖	mathematical	—	UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set.range toFun'	—	uniqueDiffOn_convex_of_isRCLikeNormedField convex_range nonempty_interior range_eq_univ_of_not_isRCLikeNormedField NormedField.nhdsNE_neBot IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul
uniqueDiffOn_preimage 📖	mathematical	IsOpen	UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set Set.instInter Set.preimage PartialEquiv.toFun symm Set.range toFun'	—	Set.inter_comm UniqueDiffOn.inter IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup uniqueDiffOn IsOpen.preimage continuous_invFun
uniqueDiffOn_preimage_source 📖	mathematical	—	UniqueDiffOn DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set Set.instInter Set.preimage PartialEquiv.toFun symm PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv Set.range toFun'	—	uniqueDiffOn_preimage OpenPartialHomeomorph.open_source
uniqueDiffWithinAt_image 📖	mathematical	—	UniqueDiffWithinAt DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set.range toFun'	—	uniqueDiffOn Set.mem_range_self

ModelWithCorners.Boundaryless

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
range_eq_univ 📖	mathematical	—	Set.range ModelWithCorners.toFun' Set.univ	—	—

ModelWithCorners.Simps

Definitions

Name	Category	Theorems
apply 📖	CompOp	—
symm_apply 📖	CompOp	—

OpenPartialHomeomorph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isManifold_singleton 📖	mathematical	PartialEquiv.source toPartialEquiv Set.univ	IsManifold singletonChartedSpace	—	IsManifold.mk' singleton_hasGroupoid instClosedUnderRestrictionContDiffGroupoid

PartialEquiv.Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
invFun 📖	mathematical	Continuous PartialEquiv.toFun PartialEquiv.symm	PartialEquiv.invFun	—	—

TopologicalSpace.Opens

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsManifoldSubtypeMem 📖	mathematical	—	IsManifold TopologicalSpace.Opens SetLike.instMembership instSetLike instTopologicalSpaceSubtype instChartedSpace	—	instHasGroupoid IsManifold.toHasGroupoid instClosedUnderRestrictionContDiffGroupoid

Topology.IsOpenEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isManifold_singleton 📖	mathematical	Topology.IsOpenEmbedding	IsManifold singletonChartedSpace	—	OpenPartialHomeomorph.isManifold_singleton

(root)

Definitions

Name	Category	Theorems
IsManifold 📖	CompData	33 math math: instIsManifoldRealEuclideanSpaceFinModelWithCornersSelfTopWithTopENatElemHAddNatOfNatSphere, TopologicalSpace.Opens.instIsManifoldSubtypeMem, instIsManifoldRealEuclideanSpaceFinOfNatNatEuclideanHalfSpaceModelWithCornersEuclideanHalfSpaceElemIcc, ContMDiffAdd.toIsManifold, SingularManifold.isManifold, ContMDiffMul.toIsManifold, instIsManifoldOfNatWithTopENatOfMinSmoothness, instIsManifoldRealEuclideanSpaceFinOfNatNatModelWithCornersSelfTopWithTopENatCircle, OpenPartialHomeomorph.isManifold_singleton, Units.instIsManifoldModelWithCornersSelf, Bundle.TotalSpace.isManifold, IsManifold.instOfTopWithTopENat, EuclideanSpace.instIsManifoldSphere, instIsManifoldMinSmoothnessOfNatWithTopENat_1, IsManifold.empty, IsManifold.disjointUnion, instIsManifoldMinSmoothnessOfNatWithTopENat, IsManifold.mk', ContinuousLinearEquiv.instIsManifoldtransContinuousLinearEquiv, IsManifold.prod, Topology.IsOpenEmbedding.isManifold_singleton, instIsManifoldModelSpace, instIsManifoldOfNatWithTopENatOfMinSmoothness_1, IsManifold.of_discreteTopology, IsManifold.instOfNatWithTopENat_1, SingularManifold.instIsManifoldRealM, IsManifold.instOfNatWithTopENat_2, IsManifold.of_le, isManifold_of_contDiffOn, UpperHalfPlane.instIsManifoldComplexModelWithCornersSelfTopWithTopENat, IsManifold.instOfSomeENatTopOfLEInfty, IsManifold.instOfNatWithTopENat, instIsManifoldIcc
ModelWithCorners 📖	CompData	—
TangentBundle 📖	CompOp	28 math math: tangentMap_chart, TangentBundle.coe_chartAt_fst, contMDiff_equivTangentBundleProd_symm, tangentBundle_model_space_coe_chartAt, equivTangentBundleProd_apply, ContMDiff.contMDiff_tangentMap, tangentMap_id, ContMDiffOn.continuousOn_tangentMapWithin, tangentBundle_model_space_coe_chartAt_symm, tangentBundleModelSpaceHomeomorph_coe, equivTangentBundleProd_symm_apply_snd, TangentBundle.chartAt, tangentBundle_model_space_chartAt, TangentBundle.mem_chart_target_iff, tangentMap_chart_symm, tangentMap_comp, tangentBundleModelSpaceHomeomorph_coe_symm, contMDiff_equivTangentBundleProd, equivTangentBundleProd_eq_tangentMap_prod_tangentMap, ContMDiffOn.contMDiffOn_tangentMapWithin, contMDiff_tangentBundleModelSpaceHomeomorph, TangentBundle.coe_chartAt_symm_fst, contMDiff_tangentBundleModelSpaceHomeomorph_symm, equivTangentBundleProd_symm_apply_proj, TangentBundle.chartAt_toPartialEquiv, ContMDiff.continuous_tangentMap, contMDiff_snd_tangentBundle_modelSpace, TangentBundle.mem_chart_source_iff
TangentSpace 📖	CompOp	232 math math: mfderiv_sumSwap, TangentBundle.continuousLinearMapAt_model_space, TangentBundle.tangentMap_tangentBundle_pure, mfderiv_prod_eq_add, instContMDiffVectorBundleOfNatWithTopENatTangentSpaceOfIsManifold, HasMFDerivAt.mul, HasMFDerivAt.add, Manifold.pathELength_eq_lintegral_mfderiv_Ioo, MDifferentiableAt.mfderiv_prod, contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt, setOf_riemmanianEDist_lt_subset_nhds, VectorField.mpullbackWithin_add, eventually_enorm_mfderivWithin_symm_extChartAt_lt, tangentMap_snd, TangentBundle.symmL_trivializationAt, VectorField.mpullbackWithin_smul, contMDiff_addInvariantVectorField, mfderiv_comp, TangentBundle.coe_chartAt_fst, SmoothBumpCovering.exists_immersion_euclidean, HasMFDerivWithinAt.prodMk, mfderiv_comp_apply_of_eq, addInvariantVectorField_smul, contMDiff_mulInvariantVectorField, contMDiff_equivTangentBundleProd_symm, hasMFDerivAt_sumSwap, TangentBundle.symmL_trivializationAt_eq_core, TangentBundle.continuousLinearMapAt_trivializationAt_eq_core, mfderiv_comp_of_eq, inTangentCoordinates_eq_mfderiv_comp, mfderivWithin_projIcc_one, tangentBundle_model_space_coe_chartAt, hasMFDerivAt_fst, mfderivWithin_comp_projIcc_one, contMDiffAt_mulInvariantVectorField, HasMFDerivAt.neg, Manifold.pathELength_def, equivTangentBundleProd_apply, VectorField.mlieBracket_zero_right, ModelWithCorners.hasMFDerivAt, HasMFDerivWithinAt.prodMap, mdifferentiableAt_addInvariantVectorField, eventually_norm_mfderivWithin_symm_extChartAt_lt, ContMDiff.contMDiff_tangentMap, HasMFDerivWithinAt.neg, hasMFDerivAt_inr, TangentBundle.trivializationAt_fst, Manifold.pathELength_eq_lintegral_mfderivWithin_Icc, mfderivWithin_sumInr, hasMFDerivAt_neg, mfderivWithin_comp_of_preimage_mem_nhdsWithin_of_eq, mfderiv_prod_eq_add_comp, eventually_riemmanianEDist_lt, mfderiv_comp_mfderivWithin, VectorField.mpullback_add_apply, hasMFDerivWithinAt_inr, IsMIntegralCurveOn.comp_mul, mdifferentiable_mulInvariantVectorField, tangentMapWithin_snd, mfderivWithin_sumInl, instContMDiffVectorBundleTopWithTopENatTangentSpaceOfIsManifold, VectorField.mpullback_smul_apply, mfderiv_sumInl, mfderiv_sub, TangentBundle.trivializationAt_apply, VectorField.mpullbackWithin_neg_apply, contMDiff_vectorSpace_iff_contDiff, mfderiv_prodMap, mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm, tangentMapWithin_proj, tangentMap_prodSnd, Diffeomorph.mfderivToContinuousLinearEquiv_coe, HasMFDerivAt.prodMap, hasMFDerivAt_id, hasMFDerivWithinAt_id, VectorField.mpullback_apply, hasMFDerivWithinAt_fst, VectorField.mpullback_zero, mfderivWithin_eventually_congr_set', ContMDiffOn.continuousOn_tangentMapWithin, VectorField.mpullbackWithin_neg, VectorField.mlieBracketWithin_zero_right, trivializationAt_model_space_apply, VectorField.mpullbackWithin_zero, mfderiv_coe_sphere_injective, mfderiv_add, mfderivWithin_comp_of_preimage_mem_nhdsWithin, TangentBundle.trivializationAt_source, OpenPartialHomeomorph.MDifferentiable.comp_symm_deriv, hasMFDerivAt_inl, IsMIntegralCurveAt.hasMFDerivAt, SmoothBumpCovering.embeddingPiTangent_injective_mfderiv, VectorField.mlieBracketWithin_self, tangentBundle_model_space_coe_chartAt_symm, equivTangentBundleProd_symm_apply_snd, OpenPartialHomeomorph.MDifferentiable.mfderiv_bijective, TangentBundle.chartAt, hasMFDerivAt_const, VectorField.mlieBracket_zero_left, VectorField.mlieBracket_swap_apply, VectorField.mpullbackWithin_smul_apply, HasMFDerivWithinAt.sum, mfderiv_prod_right, mfderivWithin_zero_of_not_mdifferentiableWithinAt, SmoothBumpCovering.embeddingPiTangent_ker_mfderiv, ModelWithCorners.hasMFDerivWithinAt, Manifold.riemannianEDist_def, HasMFDerivWithinAt.mul', TangentBundle.contMDiffVectorBundle, OpenPartialHomeomorph.MDifferentiable.range_mfderiv_eq_top, VectorField.mlieBracketWithin_swap_apply, UniqueMDiffOn.tangentBundle_proj_preimage, TangentBundle.continuousLinearMapAt_trivializationAt, tangentBundle_model_space_chartAt, TangentBundle.mem_chart_target_iff, IsLocalDiffeomorph.mfderivToContinuousLinearEquiv_coe, mfderivWithin_const, OpenPartialHomeomorph.MDifferentiable.mfderiv_surjective, hasMFDerivWithinAt_const, eventually_enorm_mfderiv_extChartAt_lt, enorm_tangentSpace_vectorSpace, oneTangentSpaceIcc_def, ModelWithCorners.hasMFDerivWithinAt_symm, mfderivWithin_prodMap, mfderiv_sumInr, HasMFDerivAt.sub, contMDiffAt_vectorSpace_iff_contDiffAt, mfderiv_snd, HasMFDerivWithinAt.add, TangentBundle.trivializationAt_eq_localTriv, mdifferentiable_addInvariantVectorField, mfderiv_zero_of_not_mdifferentiableAt, TangentSpace.vectorBundle, TangentBundle.symmL_model_space, isMIntegralCurveAt_comp_mul_ne_zero, setOf_riemannianEDist_lt_subset_nhds, range_mfderiv_coe_sphere, eventually_riemannianEDist_le_edist_extChartAt, IsMIntegralCurve.comp_mul, mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm', SmoothBumpCovering.comp_embeddingPiTangent_mfderiv, VectorField.mpullback_add, HasMFDerivAt.comp_hasMFDerivWithinAt, mfderiv_prodMk, hasMFDerivWithinAt_snd, mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt', HasMFDerivAt.prod, mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt, VectorField.mpullback_smul, contMDiff_equivTangentBundleProd, mfderiv_comp_apply, tangentMap_proj, HasMFDerivWithinAt.mul, OpenPartialHomeomorph.MDifferentiable.symm_comp_deriv, Manifold.pathELength_eq_lintegral_mfderiv_Icc, TangentBundle.trivializationAt_baseSet, norm_tangentSpace_vectorSpace, mdifferentiableAt_mulInvariantVectorField, isMIntegralCurveOn_comp_mul_ne_zero, mfderivWithin_prodMk, OpenPartialHomeomorph.MDifferentiable.mfderiv_injective, mfderivWithin_eventually_congr_set, VectorField.mpullbackWithin_apply, mfderiv_const, tangentMap_prodFst, ContMDiffOn.contMDiffOn_tangentMapWithin, eventually_norm_mfderivWithin_symm_extChartAt_comp_lt, VectorField.mpullback_neg_apply, IsMIntegralCurveAt.comp_mul_ne_zero, inverse_mfderiv_mul_left, setOf_riemmanianEDist_lt_subset_nhds', exists_embedding_euclidean_of_compact, HasMFDerivAt.prodMk, Manifold.lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc, OpenPartialHomeomorph.MDifferentiable.ker_mfderiv_eq_bot, contMDiffAt_addInvariantVectorField, contMDiff_tangentBundleModelSpaceHomeomorph, VectorField.mpullback_neg, isInvertible_mfderiv_extChartAt, VectorField.mlieBracket_swap, hasMFDerivAt_snd, HasMFDerivAt.sum, TangentBundle.coe_chartAt_symm_fst, contMDiff_tangentBundleModelSpaceHomeomorph_symm, OpenPartialHomeomorph.MDifferentiable.range_mfderiv_eq_univ, nnnorm_tangentSpace_vectorSpace, mfderiv_fst, mfderivWithin_fst, isInvertible_mfderivWithin_extChartAt_symm, mulInvariantVectorField_smul, equivTangentBundleProd_symm_apply_proj, VectorField.mlieBracketWithin_apply, IsRiemannianManifold.out, mfderiv_subtype_coe_Icc_one, HasMFDerivWithinAt.comp, TangentBundle.chartAt_toPartialEquiv, VectorField.mlieBracketWithin_zero_left, HasMFDerivAt.comp, tangentMap_prod_right, contMDiffOn_vectorSpace_iff_contDiffOn, mfderiv_neg, VectorField.mlieBracketWithin_swap, tangentMap_prod_left, IsLocalDiffeomorphAt.mfderivToContinuousLinearEquiv_coe, HasMFDerivWithinAt.prod, HasMFDerivAt.mul', mfderivWithin_id, mfderivWithin_sumSwap, mfderiv_prod_left, VectorField.mlieBracket_self, hasMFDerivWithinAt_inl, eventually_norm_mfderiv_extChartAt_lt, isMIntegralCurve_comp_mul_ne_zero, mfderiv_comp_mfderivWithin_of_eq, mulInvariantVectorField_add, instContMDiffVectorBundleSomeENatTopTangentSpaceOfIsManifold, inCoordinates_tangent_bundle_core_model_space, inverse_mfderiv_add_left, contMDiff_snd_tangentBundle_modelSpace, setOf_riemannianEDist_lt_subset_nhds', const_smul_mfderiv, HasMFDerivAt.const_smul, mfderivWithin_snd, eventually_riemannianEDist_lt, mfderiv_prod_eq_add_apply, mfderivWithin_comp, addInvariantVectorField_add, TangentBundle.mem_chart_source_iff, TangentBundle.trivializationAt_target, VectorField.mpullbackWithin_add_apply, mfderiv_id, mfderivWithin_comp_of_eq
contDiffGroupoid 📖	CompOp	17 math math: instClosedUnderRestrictionContDiffGroupoid, smoothSheafCommRing.eval_germ, contDiffGroupoid_le, IsManifold.mem_maximalAtlas_iff, symm_trans_mem_contDiffGroupoid, smoothSheafCommRing.evalHom_germ, contDiffWithinAt_localInvariantProp, contDiffWithinAt_localInvariantProp_of_le, IsManifold.toHasGroupoid, isLocalStructomorphOn_contDiffGroupoid_iff, contDiffGroupoid_zero_eq, IsManifold.compatible_of_mem_maximalAtlas, smoothSheaf.eval_germ, differentiableWithinAt_localInvariantProp, smoothSheaf.contMDiff_section, ofSet_mem_contDiffGroupoid, ContDiffGroupoid.mem_of_source_eq_empty
contDiffPregroupoid 📖	CompOp	—
instAddCommGroupTangentSpace 📖	CompOp	61 math math: TangentBundle.tangentMap_tangentBundle_pure, mfderiv_prod_eq_add, setOf_riemmanianEDist_lt_subset_nhds, eventually_enorm_mfderivWithin_symm_extChartAt_lt, VectorField.mpullbackWithin_smul, addInvariantVectorField_smul, VectorField.mlieBracketWithin_const_smul_right, HasMFDerivAt.neg, VectorField.mlieBracket_zero_right, eventually_norm_mfderivWithin_symm_extChartAt_lt, HasMFDerivWithinAt.neg, hasMFDerivAt_neg, mfderiv_prod_eq_add_comp, eventually_riemmanianEDist_lt, IsMIntegralCurveOn.comp_mul, VectorField.mpullback_smul_apply, mfderiv_sub, VectorField.mpullbackWithin_neg_apply, VectorField.mlieBracketWithin_const_smul_left, VectorField.mpullback_zero, VectorField.mpullbackWithin_neg, VectorField.mlieBracketWithin_zero_right, VectorField.mpullbackWithin_zero, VectorField.mlieBracketWithin_self, VectorField.mlieBracket_zero_left, VectorField.mlieBracket_swap_apply, VectorField.mpullbackWithin_smul_apply, HasMFDerivWithinAt.sum, VectorField.mlieBracketWithin_swap_apply, eventually_enorm_mfderiv_extChartAt_lt, enorm_tangentSpace_vectorSpace, HasMFDerivAt.sub, isMIntegralCurveAt_comp_mul_ne_zero, VectorField.mlieBracket_const_smul_left, setOf_riemannianEDist_lt_subset_nhds, eventually_riemannianEDist_le_edist_extChartAt, IsMIntegralCurve.comp_mul, HasMFDerivAt.prod, VectorField.mpullback_smul, norm_tangentSpace_vectorSpace, isMIntegralCurveOn_comp_mul_ne_zero, eventually_norm_mfderivWithin_symm_extChartAt_comp_lt, VectorField.mpullback_neg_apply, IsMIntegralCurveAt.comp_mul_ne_zero, setOf_riemmanianEDist_lt_subset_nhds', VectorField.mpullback_neg, VectorField.mlieBracket_swap, HasMFDerivAt.sum, nnnorm_tangentSpace_vectorSpace, mulInvariantVectorField_smul, IsRiemannianManifold.out, VectorField.mlieBracketWithin_zero_left, mfderiv_neg, VectorField.mlieBracketWithin_swap, HasMFDerivWithinAt.prod, VectorField.mlieBracket_self, eventually_norm_mfderiv_extChartAt_lt, isMIntegralCurve_comp_mul_ne_zero, setOf_riemannianEDist_lt_subset_nhds', eventually_riemannianEDist_lt, VectorField.mlieBracket_const_smul_right
instContinuousConstSMulTangentSpace 📖	CompOp	17 math math: setOf_riemmanianEDist_lt_subset_nhds, eventually_enorm_mfderivWithin_symm_extChartAt_lt, eventually_norm_mfderivWithin_symm_extChartAt_lt, eventually_riemmanianEDist_lt, eventually_enorm_mfderiv_extChartAt_lt, enorm_tangentSpace_vectorSpace, setOf_riemannianEDist_lt_subset_nhds, eventually_riemannianEDist_le_edist_extChartAt, norm_tangentSpace_vectorSpace, eventually_norm_mfderivWithin_symm_extChartAt_comp_lt, setOf_riemmanianEDist_lt_subset_nhds', nnnorm_tangentSpace_vectorSpace, IsRiemannianManifold.out, eventually_norm_mfderiv_extChartAt_lt, setOf_riemannianEDist_lt_subset_nhds', const_smul_mfderiv, eventually_riemannianEDist_lt
instContinuousSMulTangentSpace 📖	CompOp	1 math math: IsMIntegralCurveAt.hasMFDerivAt
instInhabitedTangentSpace 📖	CompOp	—
instIsTopologicalAddGroupTangentSpace 📖	CompOp	23 math math: mfderiv_prod_eq_add, setOf_riemmanianEDist_lt_subset_nhds, eventually_enorm_mfderivWithin_symm_extChartAt_lt, eventually_norm_mfderivWithin_symm_extChartAt_lt, mfderiv_prod_eq_add_comp, eventually_riemmanianEDist_lt, HasMFDerivWithinAt.sum, eventually_enorm_mfderiv_extChartAt_lt, enorm_tangentSpace_vectorSpace, setOf_riemannianEDist_lt_subset_nhds, eventually_riemannianEDist_le_edist_extChartAt, HasMFDerivAt.prod, norm_tangentSpace_vectorSpace, eventually_norm_mfderivWithin_symm_extChartAt_comp_lt, setOf_riemmanianEDist_lt_subset_nhds', HasMFDerivAt.sum, nnnorm_tangentSpace_vectorSpace, IsRiemannianManifold.out, mfderiv_neg, HasMFDerivWithinAt.prod, eventually_norm_mfderiv_extChartAt_lt, setOf_riemannianEDist_lt_subset_nhds', eventually_riemannianEDist_lt
instModuleTangentSpace 📖	CompOp	171 math math: mfderiv_sumSwap, TangentBundle.continuousLinearMapAt_model_space, mfderiv_prod_eq_add, instContMDiffVectorBundleOfNatWithTopENatTangentSpaceOfIsManifold, HasMFDerivAt.mul, HasMFDerivAt.add, Manifold.pathELength_eq_lintegral_mfderiv_Ioo, MDifferentiableAt.mfderiv_prod, setOf_riemmanianEDist_lt_subset_nhds, eventually_enorm_mfderivWithin_symm_extChartAt_lt, tangentMap_snd, TangentBundle.symmL_trivializationAt, VectorField.mpullbackWithin_smul, mfderiv_comp, SmoothBumpCovering.exists_immersion_euclidean, HasMFDerivWithinAt.prodMk, mfderiv_comp_apply_of_eq, addInvariantVectorField_smul, VectorField.mlieBracketWithin_const_smul_right, hasMFDerivAt_sumSwap, TangentBundle.symmL_trivializationAt_eq_core, TangentBundle.continuousLinearMapAt_trivializationAt_eq_core, mfderiv_comp_of_eq, inTangentCoordinates_eq_mfderiv_comp, mfderivWithin_projIcc_one, hasMFDerivAt_fst, mfderivWithin_comp_projIcc_one, HasMFDerivAt.neg, Manifold.pathELength_def, ModelWithCorners.hasMFDerivAt, HasMFDerivWithinAt.prodMap, eventually_norm_mfderivWithin_symm_extChartAt_lt, HasMFDerivWithinAt.neg, hasMFDerivAt_inr, Manifold.pathELength_eq_lintegral_mfderivWithin_Icc, mfderivWithin_sumInr, hasMFDerivAt_neg, mfderivWithin_comp_of_preimage_mem_nhdsWithin_of_eq, mfderiv_prod_eq_add_comp, eventually_riemmanianEDist_lt, mfderiv_comp_mfderivWithin, hasMFDerivWithinAt_inr, IsMIntegralCurveOn.comp_mul, tangentMapWithin_snd, mfderivWithin_sumInl, instContMDiffVectorBundleTopWithTopENatTangentSpaceOfIsManifold, VectorField.mpullback_smul_apply, mfderiv_sumInl, mfderiv_sub, mfderiv_prodMap, VectorField.mlieBracketWithin_const_smul_left, mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm, Diffeomorph.mfderivToContinuousLinearEquiv_coe, HasMFDerivAt.prodMap, hasMFDerivAt_id, hasMFDerivWithinAt_id, VectorField.mpullback_apply, hasMFDerivWithinAt_fst, mfderivWithin_eventually_congr_set', HasMFDerivWithinAt.hasFDerivWithinAt, mfderiv_coe_sphere_injective, mfderiv_add, mfderivWithin_comp_of_preimage_mem_nhdsWithin, OpenPartialHomeomorph.MDifferentiable.comp_symm_deriv, hasMFDerivAt_inl, IsMIntegralCurveAt.hasMFDerivAt, SmoothBumpCovering.embeddingPiTangent_injective_mfderiv, OpenPartialHomeomorph.MDifferentiable.mfderiv_bijective, hasMFDerivAt_const, VectorField.mpullbackWithin_smul_apply, HasMFDerivWithinAt.sum, mfderiv_prod_right, mfderivWithin_zero_of_not_mdifferentiableWithinAt, SmoothBumpCovering.embeddingPiTangent_ker_mfderiv, ModelWithCorners.hasMFDerivWithinAt, Manifold.riemannianEDist_def, HasMFDerivWithinAt.mul', TangentBundle.contMDiffVectorBundle, OpenPartialHomeomorph.MDifferentiable.range_mfderiv_eq_top, TangentBundle.continuousLinearMapAt_trivializationAt, IsLocalDiffeomorph.mfderivToContinuousLinearEquiv_coe, HasMFDerivAt.hasFDerivAt, mfderivWithin_const, OpenPartialHomeomorph.MDifferentiable.mfderiv_surjective, hasMFDerivWithinAt_const, eventually_enorm_mfderiv_extChartAt_lt, enorm_tangentSpace_vectorSpace, oneTangentSpaceIcc_def, ModelWithCorners.hasMFDerivWithinAt_symm, mfderivWithin_prodMap, mfderiv_sumInr, HasMFDerivAt.sub, mfderiv_snd, HasMFDerivWithinAt.add, mfderiv_zero_of_not_mdifferentiableAt, TangentSpace.vectorBundle, TangentBundle.symmL_model_space, isMIntegralCurveAt_comp_mul_ne_zero, VectorField.mlieBracket_const_smul_left, setOf_riemannianEDist_lt_subset_nhds, range_mfderiv_coe_sphere, eventually_riemannianEDist_le_edist_extChartAt, IsMIntegralCurve.comp_mul, mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm', SmoothBumpCovering.comp_embeddingPiTangent_mfderiv, HasMFDerivAt.comp_hasMFDerivWithinAt, mfderiv_prodMk, hasMFDerivWithinAt_snd, mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt', HasMFDerivAt.prod, mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt, VectorField.mpullback_smul, mfderiv_comp_apply, HasMFDerivWithinAt.mul, OpenPartialHomeomorph.MDifferentiable.symm_comp_deriv, Manifold.pathELength_eq_lintegral_mfderiv_Icc, norm_tangentSpace_vectorSpace, isMIntegralCurveOn_comp_mul_ne_zero, mfderivWithin_prodMk, OpenPartialHomeomorph.MDifferentiable.mfderiv_injective, mfderivWithin_eventually_congr_set, VectorField.mpullbackWithin_apply, mfderiv_const, hasMFDerivAt_iff_hasFDerivAt, eventually_norm_mfderivWithin_symm_extChartAt_comp_lt, IsMIntegralCurveAt.comp_mul_ne_zero, inverse_mfderiv_mul_left, setOf_riemmanianEDist_lt_subset_nhds', exists_embedding_euclidean_of_compact, HasMFDerivAt.prodMk, Manifold.lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc, OpenPartialHomeomorph.MDifferentiable.ker_mfderiv_eq_bot, isInvertible_mfderiv_extChartAt, hasMFDerivAt_snd, HasMFDerivAt.sum, OpenPartialHomeomorph.MDifferentiable.range_mfderiv_eq_univ, nnnorm_tangentSpace_vectorSpace, mfderiv_fst, mfderivWithin_fst, isInvertible_mfderivWithin_extChartAt_symm, mulInvariantVectorField_smul, VectorField.mlieBracketWithin_apply, IsRiemannianManifold.out, mfderiv_subtype_coe_Icc_one, HasMFDerivWithinAt.comp, HasMFDerivAt.comp, mfderiv_neg, IsLocalDiffeomorphAt.mfderivToContinuousLinearEquiv_coe, HasMFDerivWithinAt.prod, HasMFDerivAt.mul', mfderivWithin_id, mfderivWithin_sumSwap, mfderiv_prod_left, hasMFDerivWithinAt_inl, eventually_norm_mfderiv_extChartAt_lt, isMIntegralCurve_comp_mul_ne_zero, mfderiv_comp_mfderivWithin_of_eq, instContMDiffVectorBundleSomeENatTopTangentSpaceOfIsManifold, inCoordinates_tangent_bundle_core_model_space, hasMFDerivWithinAt_iff_hasFDerivWithinAt, inverse_mfderiv_add_left, setOf_riemannianEDist_lt_subset_nhds', const_smul_mfderiv, HasMFDerivAt.const_smul, mfderivWithin_snd, eventually_riemannianEDist_lt, mfderiv_prod_eq_add_apply, mfderivWithin_comp, VectorField.mlieBracket_const_smul_right, mfderiv_id, mfderivWithin_comp_of_eq
instPathConnectedSpaceTangentSpaceReal 📖	CompOp	—
instTopologicalSpaceTangentSpace 📖	CompOp	212 math math: mfderiv_sumSwap, TangentBundle.continuousLinearMapAt_model_space, TangentBundle.tangentMap_tangentBundle_pure, mfderiv_prod_eq_add, instContMDiffVectorBundleOfNatWithTopENatTangentSpaceOfIsManifold, HasMFDerivAt.mul, HasMFDerivAt.add, Manifold.pathELength_eq_lintegral_mfderiv_Ioo, MDifferentiableAt.mfderiv_prod, contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt, setOf_riemmanianEDist_lt_subset_nhds, VectorField.mpullbackWithin_add, eventually_enorm_mfderivWithin_symm_extChartAt_lt, tangentMap_snd, tangentMap_chart, TangentBundle.symmL_trivializationAt, VectorField.mpullbackWithin_smul, contMDiff_addInvariantVectorField, mfderiv_comp, TangentBundle.coe_chartAt_fst, SmoothBumpCovering.exists_immersion_euclidean, HasMFDerivWithinAt.prodMk, mfderiv_comp_apply_of_eq, addInvariantVectorField_smul, contMDiff_mulInvariantVectorField, contMDiff_equivTangentBundleProd_symm, hasMFDerivAt_sumSwap, TangentBundle.symmL_trivializationAt_eq_core, TangentBundle.continuousLinearMapAt_trivializationAt_eq_core, mfderiv_comp_of_eq, inTangentCoordinates_eq_mfderiv_comp, mfderivWithin_projIcc_one, tangentBundle_model_space_coe_chartAt, hasMFDerivAt_fst, mfderivWithin_comp_projIcc_one, contMDiffAt_mulInvariantVectorField, HasMFDerivAt.neg, Manifold.pathELength_def, ModelWithCorners.hasMFDerivAt, HasMFDerivWithinAt.prodMap, mdifferentiableAt_addInvariantVectorField, eventually_norm_mfderivWithin_symm_extChartAt_lt, ContMDiff.contMDiff_tangentMap, HasMFDerivWithinAt.neg, hasMFDerivAt_inr, TangentBundle.trivializationAt_fst, Manifold.pathELength_eq_lintegral_mfderivWithin_Icc, mfderivWithin_sumInr, hasMFDerivAt_neg, mfderivWithin_comp_of_preimage_mem_nhdsWithin_of_eq, mfderiv_prod_eq_add_comp, eventually_riemmanianEDist_lt, mfderiv_comp_mfderivWithin, VectorField.mpullback_add_apply, hasMFDerivWithinAt_inr, IsMIntegralCurveOn.comp_mul, mdifferentiable_mulInvariantVectorField, tangentMapWithin_snd, mfderivWithin_sumInl, instContMDiffVectorBundleTopWithTopENatTangentSpaceOfIsManifold, VectorField.mpullback_smul_apply, mfderiv_sumInl, mfderiv_sub, TangentBundle.trivializationAt_apply, contMDiff_vectorSpace_iff_contDiff, mfderiv_prodMap, mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm, Diffeomorph.mfderivToContinuousLinearEquiv_coe, HasMFDerivAt.prodMap, hasMFDerivAt_id, hasMFDerivWithinAt_id, VectorField.mpullback_apply, hasMFDerivWithinAt_fst, mfderivWithin_eventually_congr_set', HasMFDerivWithinAt.hasFDerivWithinAt, trivializationAt_model_space_apply, mfderiv_coe_sphere_injective, mfderiv_add, mfderivWithin_comp_of_preimage_mem_nhdsWithin, TangentBundle.trivializationAt_source, OpenPartialHomeomorph.MDifferentiable.comp_symm_deriv, hasMFDerivAt_inl, IsMIntegralCurveAt.hasMFDerivAt, SmoothBumpCovering.embeddingPiTangent_injective_mfderiv, tangentBundle_model_space_coe_chartAt_symm, OpenPartialHomeomorph.MDifferentiable.mfderiv_bijective, TangentBundle.chartAt, hasMFDerivAt_const, VectorField.mpullbackWithin_smul_apply, HasMFDerivWithinAt.sum, mfderiv_prod_right, mfderivWithin_zero_of_not_mdifferentiableWithinAt, SmoothBumpCovering.embeddingPiTangent_ker_mfderiv, ModelWithCorners.hasMFDerivWithinAt, Manifold.riemannianEDist_def, HasMFDerivWithinAt.mul', TangentBundle.contMDiffVectorBundle, OpenPartialHomeomorph.MDifferentiable.range_mfderiv_eq_top, UniqueMDiffOn.tangentBundle_proj_preimage, TangentBundle.continuousLinearMapAt_trivializationAt, tangentBundle_model_space_chartAt, TangentBundle.mem_chart_target_iff, IsLocalDiffeomorph.mfderivToContinuousLinearEquiv_coe, HasMFDerivAt.hasFDerivAt, mfderivWithin_const, OpenPartialHomeomorph.MDifferentiable.mfderiv_surjective, hasMFDerivWithinAt_const, eventually_enorm_mfderiv_extChartAt_lt, enorm_tangentSpace_vectorSpace, oneTangentSpaceIcc_def, ModelWithCorners.hasMFDerivWithinAt_symm, mfderivWithin_prodMap, mfderiv_sumInr, tangentMap_chart_symm, HasMFDerivAt.sub, contMDiffAt_vectorSpace_iff_contDiffAt, mfderiv_snd, HasMFDerivWithinAt.add, TangentBundle.trivializationAt_eq_localTriv, mdifferentiable_addInvariantVectorField, mfderiv_zero_of_not_mdifferentiableAt, TangentSpace.vectorBundle, TangentBundle.symmL_model_space, isMIntegralCurveAt_comp_mul_ne_zero, setOf_riemannianEDist_lt_subset_nhds, range_mfderiv_coe_sphere, eventually_riemannianEDist_le_edist_extChartAt, IsMIntegralCurve.comp_mul, mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm', SmoothBumpCovering.comp_embeddingPiTangent_mfderiv, VectorField.mpullback_add, HasMFDerivAt.comp_hasMFDerivWithinAt, mfderiv_prodMk, hasMFDerivWithinAt_snd, mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt', HasMFDerivAt.prod, mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt, VectorField.mpullback_smul, contMDiff_equivTangentBundleProd, mfderiv_comp_apply, HasMFDerivWithinAt.mul, OpenPartialHomeomorph.MDifferentiable.symm_comp_deriv, Manifold.pathELength_eq_lintegral_mfderiv_Icc, TangentBundle.trivializationAt_baseSet, norm_tangentSpace_vectorSpace, mdifferentiableAt_mulInvariantVectorField, isMIntegralCurveOn_comp_mul_ne_zero, mfderivWithin_prodMk, OpenPartialHomeomorph.MDifferentiable.mfderiv_injective, mfderivWithin_eventually_congr_set, VectorField.mpullbackWithin_apply, mfderiv_const, hasMFDerivAt_iff_hasFDerivAt, ContMDiffOn.contMDiffOn_tangentMapWithin, eventually_norm_mfderivWithin_symm_extChartAt_comp_lt, IsMIntegralCurveAt.comp_mul_ne_zero, inverse_mfderiv_mul_left, setOf_riemmanianEDist_lt_subset_nhds', exists_embedding_euclidean_of_compact, HasMFDerivAt.prodMk, Manifold.lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc, OpenPartialHomeomorph.MDifferentiable.ker_mfderiv_eq_bot, contMDiffAt_addInvariantVectorField, contMDiff_tangentBundleModelSpaceHomeomorph, isInvertible_mfderiv_extChartAt, hasMFDerivAt_snd, HasMFDerivAt.sum, TangentBundle.coe_chartAt_symm_fst, contMDiff_tangentBundleModelSpaceHomeomorph_symm, OpenPartialHomeomorph.MDifferentiable.range_mfderiv_eq_univ, nnnorm_tangentSpace_vectorSpace, mfderiv_fst, mfderivWithin_fst, isInvertible_mfderivWithin_extChartAt_symm, mulInvariantVectorField_smul, VectorField.mlieBracketWithin_apply, IsRiemannianManifold.out, mfderiv_subtype_coe_Icc_one, HasMFDerivWithinAt.comp, TangentBundle.chartAt_toPartialEquiv, HasMFDerivAt.comp, contMDiffOn_vectorSpace_iff_contDiffOn, mfderiv_neg, IsLocalDiffeomorphAt.mfderivToContinuousLinearEquiv_coe, HasMFDerivWithinAt.prod, HasMFDerivAt.mul', mfderivWithin_id, mfderivWithin_sumSwap, mfderiv_prod_left, hasMFDerivWithinAt_inl, eventually_norm_mfderiv_extChartAt_lt, isMIntegralCurve_comp_mul_ne_zero, mfderiv_comp_mfderivWithin_of_eq, mulInvariantVectorField_add, instContMDiffVectorBundleSomeENatTopTangentSpaceOfIsManifold, inCoordinates_tangent_bundle_core_model_space, hasMFDerivWithinAt_iff_hasFDerivWithinAt, inverse_mfderiv_add_left, contMDiff_snd_tangentBundle_modelSpace, setOf_riemannianEDist_lt_subset_nhds', const_smul_mfderiv, HasMFDerivAt.const_smul, mfderivWithin_snd, eventually_riemannianEDist_lt, mfderiv_prod_eq_add_apply, mfderivWithin_comp, addInvariantVectorField_add, TangentBundle.mem_chart_source_iff, TangentBundle.trivializationAt_target, VectorField.mpullbackWithin_add_apply, mfderiv_id, mfderivWithin_comp_of_eq
modelWithCornersSelf 📖	CompOp	420 math math: TangentBundle.continuousLinearMapAt_model_space, ContMDiffAt.coordChangeL, MDifferentiable.coordChangeL, UpperHalfPlane.mdifferentiable_num, Bundle.ContMDiffRiemannianMetric.contMDiff, Bundle.mdifferentiableAt_proj, SmoothBumpCovering.toSmoothPartitionOfUnity_eq_mul_prod, Trivialization.mdifferentiableAt_section_iff, LeftInvariantDerivation.lift_zero, exists_contMDiffMap_zero_one_of_isClosed, contMDiffAt_extend, CuspFormClass.holo, instIsManifoldRealEuclideanSpaceFinModelWithCornersSelfTopWithTopENatElemHAddNatOfNatSphere, LeftInvariantDerivation.leibniz, contMDiffWithinAt_iff_target, Bundle.contMDiffOn_zeroSection, ContMDiffMap.coeFnAlgHom_apply, Manifold.pathELength_eq_lintegral_mfderiv_Ioo, ContDiffWithinAt.contMDiffWithinAt, mdifferentiableWithinAt_totalSpace, contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt, smoothSheafCommRing.nonunits_stalk, MDifferentiableWithinAt.differentiableWithinAt_mpullbackWithin_vectorField, contDiffWithinAtProp_self, ContDiffAt.contMDiffAt, mdifferentiable_iff_target, contMDiffAt_iff_source, ContinuousLinearEquiv.symm_toDiffeomorph, eventually_enorm_mfderivWithin_symm_extChartAt_lt, LeftInvariantDerivation.coe_derivation, TangentBundle.symmL_trivializationAt, SmoothPartitionOfUnity.locallyFinite, exists_smooth_one_nhds_of_subset_interior, ContMDiffWithinAt.mfderivWithin_const, SmoothPartitionOfUnity.nonneg, LeftInvariantDerivation.left_invariant', Trivialization.mdifferentiableOn_section_baseSet_iff, mdifferentiableOn_extChartAt, contMDiff_neg_sphere, mdifferentiableOn_symm_coordChangeL, SmoothBumpCovering.exists_immersion_euclidean, IsOpen.exists_msmooth_support_eq, SmoothPartitionOfUnity.locallyFinite', ModelWithCorners.mdifferentiableOn_symm, Bundle.contMDiffWithinAt_zeroSection, ContinuousLinearEquiv.coe_toDiffeomorph_symm, hasMFDerivAt_extChartAt, ContinuousLinearMap.contMDiff, ContinuousLinearMap.mdifferentiable, instContMDiffAddSelf, smoothSheafCommRing.instLocalRing_stalk, modelWithCornersSelf_coe_symm, mdifferentiableWithinAt_section, Trivialization.contMDiffAt_iff, VectorBundleCore.contMDiffOn_coordChange, Trivialization.contMDiffOn_symm_trans, inTangentCoordinates_eq_mfderiv_comp, mfderivWithin_projIcc_one, Trivialization.contMDiff_iff, LeftInvariantDerivation.lift_add, Trivialization.contMDiffOn_section_iff, Trivialization.mdifferentiableWithinAt_snd_comp_iff₂, contMDiffOn_iff_contDiffOn, mfderivWithin_comp_projIcc_one, UpperHalfPlane.mdifferentiable_inv_denom, LeftInvariantDerivation.lift_smul, SmoothPartitionOfUnity.sum_finsupport', Bundle.contMDiffAt_zeroSection, Manifold.pathELength_def, contMDiffWithinAt_prod_module_iff, ModelWithCorners.hasMFDerivAt, instNormedSpaceLieAddGroup, eventually_norm_mfderivWithin_symm_extChartAt_lt, VectorField.mpullback_eq_pullback, UpperHalfPlane.contMDiff_coe, CuspForm.holo', contMDiff_coe_sphere, LeftInvariantDerivation.comp_L, IsOpen.exists_contMDiff_support_eq_aux, modelWithCornersSelf_boundaryless, Manifold.pathELength_eq_lintegral_mfderivWithin_Icc, hasMFDerivAt_neg, ContinuousLinearEquiv.hasMFDerivAt, instIsManifoldRealEuclideanSpaceFinOfNatNatModelWithCornersSelfTopWithTopENatCircle, SmoothBumpCovering.toSmoothPartitionOfUnity_apply, SmoothPartitionOfUnity.contDiffAt_finsum, mdifferentiableOn_iff_target, contMDiff_model, ContinuousLinearEquiv.hasMFDerivWithinAt, ContDiffOn.contMDiffOn, UpperHalfPlane.contMDiff_inv_denom, hasMFDerivWithinAt_extChartAt, contMDiffWithinAt_pi_space, mdifferentiableAt_totalSpace, UniqueMDiffOn.uniqueMDiffOn_target_inter, mdifferentiableOn_prod_module_iff, contMDiffAt_iff_source_of_mem_source, Metric.exists_smooth_forall_closedBall_subset, instLieGroupRealEuclideanSpaceFinOfNatNatModelWithCornersSelfTopWithTopENatCircle, DifferentiableWithinAt.mdifferentiableWithinAt, Units.instIsManifoldModelWithCornersSelf, LeftInvariantDerivation.evalAt_coe, Trivialization.mdifferentiableAt_totalSpace_iff, ContMDiffOn.coordChangeL, mdifferentiableAt_hom_bundle, SmoothPartitionOfUnity.le_one, Continuous.exists_contMDiff_approx, exists_contMDiffMap_zero_one_nhds_of_isClosed, contMDiffOn_pi_space, Bundle.TotalSpace.isManifold, UniqueDiffWithinAt.uniqueMDiffWithinAt, ContMDiffAt.mfderiv_const, smoothSheafCommRing.isUnit_stalk_iff, contMDiff_vectorSpace_iff_contDiff, LeftInvariantDerivation.map_zero, EuclideanSpace.instIsManifoldSphere, TangentBundle.coordChange_model_space, fdifferential_apply, SmoothBumpFunction.contMDiffAt, MDifferentiableOn.coordChangeL, UniqueMDiffWithinAt.bundle_preimage', mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm, ContMDiffMap.smul_comp, IsContMDiffRiemannianBundle.exists_contMDiff, SmoothBumpCovering.sum_toSmoothPartitionOfUnity_eq, contMDiffAt_coordChangeL, contMDiff_subtype_coe_Icc, LeftInvariantDerivation.coe_sub, MDifferentiableWithinAt.coordChangeL, Units.instLieGroupModelWithCornersSelf, contDiffWithinAtProp_self_source, LeftInvariantDerivation.left_invariant'', contMDiff_iff_contDiff, contMDiff_iff_target, mdifferentiableOn_extChartAt_symm, UpperHalfPlane.contMDiff_num, SmoothPartitionOfUnity.sum_eq_one', VectorField.mlieBracketWithin_def, UpperHalfPlane.mdifferentiable_denom, mdifferentiableAt_prod_module_iff, writtenInExtChartAt_model_space, contMDiffOn_extChartAt, Trivialization.contMDiffOn_localFrame_baseSet, SmoothPartitionOfUnity.mem_finsupport, IsOpen.exists_contMDiff_support_eq, DifferentiableOn.mdifferentiableOn, ContinuousLinearEquiv.mdifferentiableOn, mdifferentiableWithinAt_iff_differentiableWithinAt, contMDiff_smul, contMDiffOn_continuousLinearMapCoordChange, mfderiv_coe_sphere_injective, contMDiffOn_extChartAt_symm, Bundle.mdifferentiableWithinAt_proj, IsLocalFrameOn.contMDiffOn, contMDiffWithinAt_extChartAt_symm_range_self, ContinuousLinearMap.mfderiv_eq, contMDiffWithinAt_iff_target_of_mem_source, Bundle.contMDiffWithinAt_totalSpace, contMDiffWithinAt_iff_source_of_mem_maximalAtlas, IsMIntegralCurveAt.hasMFDerivAt, Bundle.mdifferentiableOn_proj, SmoothBumpCovering.embeddingPiTangent_injective_mfderiv, ModelWithCorners.mdifferentiableAt, exists_msmooth_support_eq_eq_one_iff, SmoothPartitionOfUnity.coe_finsupport, Emetric.exists_contMDiffMap_forall_closedBall_subset, differentiableWithinAtProp_self_source, Diffeomorph.contDiff, contMDiffOn_symm_coordChangeL, Metric.exists_contMDiffMap_forall_closedBall_subset, IsLocalFrameOn.contMDiffAt, contMDiffAt_hom_bundle, exists_msmooth_zero_iff_one_iff_of_isClosed, LeftInvariantDerivation.map_add, SmoothPartitionOfUnity.finsum_smul_mem_convex, FiberBundle.extChartAt, LeftInvariantDerivation.coe_add, ContDiff.contMDiff, SmoothPartitionOfUnity.sum_le_one', instIsRiemannianManifoldModelWithCornersSelfReal, SmoothBumpCovering.embeddingPiTangent_ker_mfderiv, ModelWithCorners.hasMFDerivWithinAt, SmoothPartitionOfUnity.sum_nonneg, Bundle.contMDiffWithinAt_proj, modelWithCornersSelf_prod, Bundle.contMDiffAt_totalSpace, Diffeomorph.uniqueDiffOn_image, LeftInvariantDerivation.coe_injective, UpperHalfPlane.contMDiff_denom_zpow, SmoothBumpCovering.exists_finset_toSmoothPartitionOfUnity_eventuallyEq, ContinuousLinearMap.mdifferentiableWithinAt, LeftInvariantDerivation.coe_neg, Trivialization.contMDiffOn_section_baseSet_iff, TangentBundle.continuousLinearMapAt_trivializationAt, contMDiffWithinAt_comp_projIcc_iff, mdifferentiableAt_iff_target_of_mem_source, ContMDiffWithinAt.mfderivWithin, IsOpen.exists_msmooth_support_eq_aux, ext_chart_model_space_apply, exists_contMDiff_zero_iff_one_iff_of_isClosed, Bundle.contMDiffOn_proj, contDiffWithinAtProp_self_target, writtenInExtChartAt_extChartAt, Bundle.contMDiff_proj, contMDiffAt_iff_target_of_mem_source, ContMDiffMap.coe_smul, ContinuousLinearMap.hasMFDerivAt, mdifferentiableOn_continuousLinearMapCoordChange, mfderivWithin_eq_fderivWithin, VectorField.eventuallyEq_mpullback_mpullbackWithin_extChartAt, extChartAt_model_space_eq_id, eventually_enorm_mfderiv_extChartAt_lt, enorm_tangentSpace_vectorSpace, DifferentiableWithinAtProp_self, LeftInvariantDerivation.map_smul, oneTangentSpaceIcc_def, contMDiffAt_section_of_mem_baseSet, ModelWithCorners.uniqueMDiffOn, ModelWithCorners.hasMFDerivWithinAt_symm, SmoothPartitionOfUnity.sum_eq_one, mdifferentiableAt_neg, instContMDiffInv₀ModelWithCornersSelf, contMDiffOn_iff_source_of_mem_maximalAtlas, SmoothBumpCovering.embeddingPiTangent_injOn, contMDiffWithinAt_extChartAt_symm_target_self, UniqueMDiffWithinAt.bundle_preimage, contMDiffAt_vectorSpace_iff_contDiffAt, contMDiffWithinAt_iff_contDiffWithinAt, PointedContMDiffMap.instIsScalarTowerSomeENatTopContMDiffMapModelWithCornersSelf, Bundle.mdifferentiableWithinAt_zeroSection, LeftInvariantDerivation.coe_smul, ContinuousLinearEquiv.mdifferentiableWithinAt, ContinuousLinearEquiv.mdifferentiable, writtenInExtChartAt_extChartAt_symm, mdifferentiableWithinAt_comp_projIcc_iff, VectorField.contMDiffWithinAt_mpullbackWithin_extChartAt_symm, mdifferentiableWithinAt_iff_source_of_mem_maximalAtlas, mdifferentiableOn_iff_differentiableOn, TangentBundle.symmL_model_space, Differentiable.mdifferentiable, range_mfderiv_coe_sphere, uniqueMDiffOn_iff_uniqueDiffOn, contMDiffAt_extChartAt, mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm', SmoothBumpCovering.comp_embeddingPiTangent_mfderiv, ContinuousLinearEquiv.mfderiv_eq, Trivialization.mdifferentiableWithinAt_section_iff, mdifferentiableOn_coordChangeL, contMDiffWithinAt_extChartAt_symm_target, Bundle.contMDiff_zeroSection, FiberBundle.extChartAt_target, contMDiffAt_localFrame_of_mem, ContMDiffVectorBundle.contMDiffOn_coordChangeL, contMDiff_prod_module_iff, VectorBundleCore.IsContMDiff.contMDiffOn_coordChange, mdifferentiableAt_section, mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt', SmoothPartitionOfUnity.exists_pos_of_mem, Bundle.mdifferentiable_proj, exists_smooth_zero_one_of_isClosed, ModelWithCorners.mdifferentiable, MDifferentiableAt.coordChangeL, mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt, Diffeomorph.uniqueDiffOn_preimage, SmoothBumpCovering.embeddingPiTangent_injective, exists_contMDiff_support_eq_eq_one_iff, ContMDiffSection.contMDiff, LeftInvariantDerivation.map_sub, SmoothPartitionOfUnity.sum_finsupport_smul_eq_finsum, LeftInvariantDerivation.map_neg, Trivialization.contMDiffWithinAt_iff, UniqueMDiffOn.bundle_preimage, contMDiffWithinAt_iff_source, Bundle.contMDiffAt_section, SmoothPartitionOfUnity.sum_finsupport, contMDiffWithinAt_iff_source_of_mem_source, ContinuousLinearEquiv.coe_toDiffeomorph, exists_smooth_forall_mem_convex_of_local_const, VectorField.mpullbackWithin_eq_pullbackWithin, Manifold.pathELength_eq_lintegral_mfderiv_Icc, norm_tangentSpace_vectorSpace, mdifferentiableAt_iff_source_of_mem_source, contMDiffAt_prod_module_iff, IsManifold.of_discreteTopology, Trivialization.mdifferentiableOn_section_iff, mdifferentiable_jacobiTheta, SmoothBumpCovering.support_toSmoothPartitionOfUnity_subset, hasMFDerivAt_iff_hasFDerivAt, mdifferentiableAt_iff_differentiableAt, mdifferentiableWithinAt_iff_target_of_mem_source, mdifferentiableWithinAt_extChartAt_symm, contMDiffOn_comp_projIcc_iff, SmoothBumpFunction.contMDiff, ModelWithCorners.mdifferentiableOn, modelWithCornersSelf_partialEquiv, contMDiffWithinAt_extChartAt_symm_range, ContMDiffWithinAt.coordChangeL, UpperHalfPlane.contMDiffAt_ofComplex, eventually_norm_mfderivWithin_symm_extChartAt_comp_lt, ModularForm.holo', SmoothPartitionOfUnity.finite_tsupport, Trivialization.contMDiffAt_section_iff, ContMDiffMap.smul_comp', ContMDiffAt.mfderiv, LeftInvariantDerivation.coe_zero, Trivialization.mdifferentiableAt_snd_comp_iff₂, UpperHalfPlane.contMDiffAt_iff, contMDiffOn_extend_symm, UpperHalfPlane.instIsManifoldComplexModelWithCornersSelfTopWithTopENat, exists_embedding_euclidean_of_compact, VectorPrebundle.contMDiffOn_contMDiffCoordChange, LeftInvariantDerivation.toDerivation_injective, ContinuousLinearMap.contMDiffWithinAt, mdifferentiableAt_coordChangeL, mdifferentiableWithinAt_iff_source_of_mem_source, UpperHalfPlane.mdifferentiable_coe, Trivialization.contMDiffOn_symm, Bundle.contMDiffAt_proj, Trivialization.contMDiffOn_iff, Units.contMDiff_val, contMDiff_tangentBundleModelSpaceHomeomorph, modelWithCornersSelf_coe, SmoothPartitionOfUnity.mem_fintsupport_iff, Emetric.exists_smooth_forall_closedBall_subset, isInvertible_mfderiv_extChartAt, ModularFormClass.holo, mdifferentiableWithinAt_prod_module_iff, mdifferentiableAt_iff_target, contMDiff_pi_space, contMDiffAt_extChartAt', uniqueMDiffWithinAt_iff_uniqueDiffWithinAt, ContinuousLinearMap.hasMFDerivWithinAt, Bundle.contMDiffWithinAt_section, VectorPrebundle.IsContMDiff.exists_contMDiffCoordChange, Bundle.mdifferentiableOn_zeroSection, Trivialization.mdifferentiableWithinAt_totalSpace_iff, ContMDiffSection.mdifferentiable', contMDiff_tangentBundleModelSpaceHomeomorph_symm, ContinuousLinearMap.contMDiffOn, contMDiffOn_coordChangeL, contMDiffOn_model_symm, nnnorm_tangentSpace_vectorSpace, mfderiv_eq_fderiv, EisensteinSeries.eisensteinSeries_SIF_MDifferentiable, ContinuousLinearMap.mdifferentiableOn, ContMDiffSection.mdifferentiableAt, LeftInvariantDerivation.commutator_apply, UpperHalfPlane.mdifferentiableAt_iff, LeftInvariantDerivation.commutator_coe_derivation, instFieldContMDiffRing, isInvertible_mfderivWithin_extChartAt_symm, mdifferentiable_prod_module_iff, VectorField.mlieBracketWithin_apply, ContMDiffSection.mdifferentiable, SmoothPartitionOfUnity.toPartitionOfUnity_toFun, Bundle.mdifferentiable_zeroSection, LeftInvariantDerivation.ext_iff, mfderiv_subtype_coe_Icc_one, VectorField.mlieBracketWithin_eq_lieBracketWithin, VectorField.eventually_contMDiffWithinAt_mpullbackWithin_extChartAt_symm, DifferentiableAt.mdifferentiableAt, contMDiffAt_pi_space, exists_smooth_zero_one_nhds_of_isClosed, contMDiffOn_iff_target, contMDiffOn_vectorSpace_iff_contDiffOn, mfderiv_neg, UpperHalfPlane.contMDiff_smul, contMDiffAt_iff_target, LeftInvariantDerivation.toFun_eq_coe, UpperHalfPlane.contMDiff_denom, Manifold.exists_lt_of_riemannianEDist_lt, SmoothBumpCovering.embeddingPiTangent_coe, EisensteinSeries.eisensteinSeriesSIF_mdifferentiable, SmoothPartitionOfUnity.nonneg', ContMDiffSection.contMDiff_toFun, UpperHalfPlane.mdifferentiable_denom_zpow, exists_contMDiffMap_one_nhds_of_subset_interior, SmoothPartitionOfUnity.sum_le_one, ModelWithCorners.mdifferentiableWithinAt_symm, contMDiffOn_prod_module_iff, eventually_norm_mfderiv_extChartAt_lt, mdifferentiableWithinAt_hom_bundle, Trivialization.contMDiffOn, UpperHalfPlane.mdifferentiable_iff, contMDiffOn_section_of_mem_baseSet₀, exists_contMDiffMap_forall_mem_convex_of_local_const, smooth_functions_tower, mdifferentiable_iff_differentiable, Bundle.mdifferentiableAt_zeroSection, Manifold.exists_lt_locally_constant_of_riemannianEDist_lt, ContinuousLinearEquiv.mdifferentiableAt, UniqueDiffOn.uniqueMDiffOn, mdifferentiableAt_extChartAt, Trivialization.mdifferentiable, UpperHalfPlane.mdifferentiableAt_ofComplex, hasMFDerivWithinAt_iff_hasFDerivWithinAt, LeftInvariantDerivation.instLinearMapClassContMDiffMapModelWithCornersSelfSomeENatTop, LeftInvariantDerivation.coeFnAddMonoidHom_apply, contMDiff_snd_tangentBundle_modelSpace, contMDiffWithinAt_hom_bundle, mem_contMDiffFiberwiseLinear_iff, ContinuousLinearMap.contMDiffAt, contMDiffAt_iff_contDiffAt, Derivation.evalAt_apply, mdifferentiableWithinAt_iff_target, differentiableWithinAtProp_self_target, ContinuousLinearMap.mdifferentiableAt, Trivialization.contMDiffWithinAt_section, SmoothBumpCovering.toSmoothPartitionOfUnity_zero_of_zero, ContMDiff.coordChangeL, SmoothPartitionOfUnity.contMDiff_sum, contMDiffOn_projIcc, Trivialization.contMDiffWithinAt_snd_comp_iff₂, Metric.exists_contMDiffMap_forall_closedEBall_subset, contMDiff_circleExp, ContMDiffMap.coeFnLinearMap_apply, UpperHalfPlane.mdifferentiable_smul, contMDiffOn_section_of_mem_baseSet, ModelWithCorners.mdifferentiableWithinAt, LeftInvariantDerivation.evalAt_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contDiffGroupoid_le 📖	mathematical	WithTop ENat Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat	StructureGroupoid StructureGroupoid.partialOrder contDiffGroupoid	—	contDiffGroupoid.eq_1 groupoid_of_pregroupoid_le ContDiffOn.of_le
contDiffGroupoid_prod 📖	mathematical	OpenPartialHomeomorph StructureGroupoid instMembershipOpenPartialHomeomorphStructureGroupoid contDiffGroupoid	instTopologicalSpaceProd ModelProd instTopologicalSpaceModelProd Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelWithCorners.prod OpenPartialHomeomorph.prod	—	ContDiffOn.prodMap ModelWithCorners.image_eq Set.prod_image_image_eq
contDiffGroupoid_zero_eq 📖	mathematical	—	contDiffGroupoid WithTop ENat WithTop.zero instZeroENat continuousGroupoid	—	le_antisymm le_top contDiffGroupoid.eq_1 mem_groupoid_of_pregroupoid contDiffPregroupoid.eq_1 Continuous.comp_continuousOn ModelWithCorners.continuous ContinuousOn.comp OpenPartialHomeomorph.continuousOn ModelWithCorners.continuousOn_symm Set.MapsTo.mono_left Set.mapsTo_preimage Set.inter_subset_left
instClosedUnderRestrictionContDiffGroupoid 📖	mathematical	—	ClosedUnderRestriction contDiffGroupoid	—	closedUnderRestriction_iff_id_le StructureGroupoid.le_iff StructureGroupoid.mem_of_eqOnSource' ofSet_mem_contDiffGroupoid
instIsManifoldModelSpace 📖	mathematical	—	IsManifold chartedSpaceSelf	—	hasGroupoid_model_space
isManifold_of_contDiffOn 📖	mathematical	ContDiffOn ModelWithCorners.toFun' OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.trans OpenPartialHomeomorph.symm PartialEquiv.toFun ModelWithCorners.symm Set Set.instInter Set.preimage PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv Set.range	IsManifold	—	StructureGroupoid.compatible hasGroupoid_of_pregroupoid
modelWithCornersSelf_boundaryless 📖	mathematical	—	ModelWithCorners.Boundaryless UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf	—	Set.range_id
modelWithCornersSelf_coe 📖	mathematical	—	ModelWithCorners.toFun' UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf	—	—
modelWithCornersSelf_coe_symm 📖	mathematical	—	PartialEquiv.toFun ModelWithCorners.symm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf	—	—
modelWithCornersSelf_partialEquiv 📖	mathematical	—	ModelWithCorners.toPartialEquiv UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf PartialEquiv.refl	—	—
modelWithCornersSelf_prod 📖	mathematical	—	modelWithCornersSelf Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelWithCorners.prod UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	ModelWithCorners.ext PartialEquiv.refl_prod_refl
modelWithCorners_prod_coe 📖	mathematical	—	ModelWithCorners.toFun' Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd ModelWithCorners.prod	—	—
modelWithCorners_prod_coe_symm 📖	mathematical	—	PartialEquiv.toFun ModelProd ModelWithCorners.symm Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup instTopologicalSpaceModelProd ModelWithCorners.prod	—	—
modelWithCorners_prod_toPartialEquiv 📖	mathematical	—	ModelWithCorners.toPartialEquiv Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd ModelWithCorners.prod PartialEquiv.prod	—	—
ofSet_mem_contDiffGroupoid 📖	mathematical	IsOpen	OpenPartialHomeomorph StructureGroupoid instMembershipOpenPartialHomeomorphStructureGroupoid contDiffGroupoid OpenPartialHomeomorph.ofSet	—	contDiffGroupoid.eq_1 mem_groupoid_of_pregroupoid ContDiff.contDiffOn contDiff_id ContDiffOn.congr_mono ModelWithCorners.right_inv Set.subset_univ CompTriple.comp_eq CompTriple.instId_comp CompTriple.instIsIdId
symm_trans_mem_contDiffGroupoid 📖	mathematical	—	OpenPartialHomeomorph StructureGroupoid instMembershipOpenPartialHomeomorphStructureGroupoid contDiffGroupoid OpenPartialHomeomorph.trans OpenPartialHomeomorph.symm	—	StructureGroupoid.mem_of_eqOnSource OpenPartialHomeomorph.open_target ofSet_mem_contDiffGroupoid OpenPartialHomeomorph.symm_trans_self

---

← Back to Index