ChartedSpace

📁 Source: Mathlib/Geometry/Manifold/ChartedSpace.lean

Statistics

Metric	Count
Definitions ChartedSpace, atlas, chartAt, comp, empty, of_discreteTopology, sum, sum_of_nonempty, ChartedSpaceCore, atlas, chartAt, openPartialHomeomorph, toChartedSpace, toTopologicalSpace, Manifold_type_tags, ModelPi, ModelProd, achart, atlas, chartAt, chartedSpaceSelf, instTopologicalSpaceModelPi, instTopologicalSpaceModelProd, modelPiInhabited, modelProdInhabited, piChartedSpace, prodChartedSpace	27
Theorems chart_mem_atlas, discreteTopology, ext, ext_iff, isOpen_iff, locPathConnectedSpace, locallyCompactSpace, locallyConnectedSpace, mem_atlas_sum, mem_chart_source, secondCountable_of_countable_cover, secondCountable_of_sigmaCompact, sum_chartAt_inl, sum_chartAt_inr, t1Space, chart_mem_atlas, continuousOn_toFun, mem_chart_source, open_source, open_source', open_target, ext, ext_iff, achart_def, achart_val, chartAt_comp, chartAt_self_eq, chart_mem_atlas, chart_source_mem_nhds, chart_target_mem_nhds, chartedSpaceSelf_atlas, chartedSpaceSelf_prod, chartedSpace_of_discreteTopology_chartAt, coe_achart, iUnion_source_chartAt, isEmpty_of_chartedSpace, mem_achart_source, mem_chart_source, mem_chart_target, modelProd_range_prod_id, nonempty_of_chartedSpace, piChartedSpace_chartAt, prodChartedSpace_chartAt, sum_chartAt_inl_apply, sum_chartAt_inr_apply	45
Total	72

ChartedSpace

Definitions

Name	Category	Theorems
atlas 📖	CompOp	2 math math: chart_mem_atlas, ext_iff
chartAt 📖	CompOp	3 math math: chart_mem_atlas, mem_chart_source, ext_iff
comp 📖	CompOp	5 math math: writtenInExtChartAt_chartAt_comp, StructureGroupoid.HasGroupoid.comp, chartAt_comp, writtenInExtChartAt_chartAt_symm_comp, extChartAt_comp
empty 📖	CompOp	—
of_discreteTopology 📖	CompOp	2 math math: chartedSpace_of_discreteTopology_chartAt, IsManifold.of_discreteTopology
sum 📖	CompOp	45 math math: mfderiv_sumSwap, sum_chartAt_inr, contMDiff_sum_map, ModelWithCorners.interior_disjointUnion, hasMFDerivAt_sumSwap, extChartAt_inl_apply, ContMDiff.inr, Diffeomorph.sumCongr_symm_symm, hasMFDerivAt_inr, mfderivWithin_sumInr, Diffeomorph.sumAssoc_coe, ModelWithCorners.boundaryPoint_inl, Diffeomorph.sumCongr_inl, ContMDiff.sumMap, hasMFDerivWithinAt_inr, mfderivWithin_sumInl, ContMDiff.inl, mfderiv_sumInl, ModelWithCorners.boundary_disjointUnion, sum_chartAt_inl, Diffeomorph.sumComm_coe, Diffeomorph.sumComm_inr, ContMDiff.swap, extChartAt_inr_apply, Diffeomorph.sumCongr_coe, hasMFDerivAt_inl, IsManifold.disjointUnion, Diffeomorph.sumCongr_inr, Diffeomorph.sumEmpty_apply_inl, ModelWithCorners.boundaryPoint_inr, ModelWithCorners.boundaryless_disjointUnion, mfderiv_sumInr, ContMDiff.sumElim, writtenInExtChartAt_sumSwap_eventuallyEq_id, Diffeomorph.sumEmpty_toEquiv, Diffeomorph.sumComm_inl, writtenInExtChartAt_sumInr_eventuallyEq_id, mfderivWithin_sumSwap, hasMFDerivWithinAt_inl, Diffeomorph.sumComm_symm, sum_chartAt_inl_apply, writtenInExtChartAt_sumInl_eventuallyEq_id, ModelWithCorners.interiorPoint_inl, ModelWithCorners.interiorPoint_inr, sum_chartAt_inr_apply
sum_of_nonempty 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
chart_mem_atlas 📖	mathematical	—	OpenPartialHomeomorph Set Set.instMembership atlas chartAt	—	—
discreteTopology 📖	mathematical	—	DiscreteTopology	—	discreteTopology_iff_isOpen_singleton OpenPartialHomeomorph.isOpen_inter_preimage isOpen_discrete Set.Subset.antisymm OpenPartialHomeomorph.injOn mem_chart_source
ext 📖	—	atlas chartAt	—	—	—
ext_iff 📖	mathematical	—	atlas chartAt	—	ext
isOpen_iff 📖	mathematical	—	IsOpen Set.image OpenPartialHomeomorph.toFun' chartAt Set Set.instInter PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv	—	isOpen_iff_of_cover OpenPartialHomeomorph.open_source iUnion_source_chartAt OpenPartialHomeomorph.isOpen_image_iff_of_subset_source Set.inter_subset_left
locPathConnectedSpace 📖	mathematical	—	LocPathConnectedSpace	—	Filter.inter_mem chart_source_mem_nhds OpenPartialHomeomorph.left_inv mem_chart_source OpenPartialHomeomorph.image_mem_nhds pathComponentIn_mem_nhds IsPathConnected.image' isPathConnected_pathComponentIn Set.mem_image_of_mem mem_of_mem_nhds ContinuousOn.mono OpenPartialHomeomorph.continuousOn_symm subset_trans Set.instIsTransSubset HasSubset.Subset.trans pathComponentIn_mono Set.image_mono Set.inter_subset_right pathComponentIn_subset OpenPartialHomeomorph.map_source'' Eq.subset Set.instReflSubset PartialEquiv.symm_image_image_of_subset_source Set.inter_subset_left Filter.mem_of_superset
locallyCompactSpace 📖	mathematical	—	LocallyCompactSpace	—	OpenPartialHomeomorph.symm_map_nhds_eq mem_chart_source Filter.HasBasis.map Filter.HasBasis.hasBasis_self_subset compact_basis_nhds chart_target_mem_nhds LocallyCompactSpace.of_hasBasis IsCompact.image_of_continuousOn ContinuousOn.mono OpenPartialHomeomorph.continuousOn_symm
locallyConnectedSpace 📖	mathematical	—	LocallyConnectedSpace	—	locallyConnectedSpace_of_connected_bases Set.image_congr OpenPartialHomeomorph.symm_map_nhds_eq Filter.HasBasis.map Filter.HasBasis.restrict_subset LocallyConnectedSpace.open_connected_basis IsOpen.mem_nhds OpenPartialHomeomorph.open_target mem_chart_target IsPreconnected.image IsConnected.isPreconnected ContinuousOn.mono OpenPartialHomeomorph.continuousOn_symm
mem_atlas_sum 📖	mathematical	OpenPartialHomeomorph instTopologicalSpaceSum Set Set.instMembership atlas sum	OpenPartialHomeomorph Set Set.instMembership atlas OpenPartialHomeomorph.lift_openEmbedding instTopologicalSpaceSum Topology.IsOpenEmbedding.inl Topology.IsOpenEmbedding.inr	—	Topology.IsOpenEmbedding.inl Topology.IsOpenEmbedding.inr instIsEmptySum
mem_chart_source 📖	mathematical	—	Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv chartAt	—	—
secondCountable_of_countable_cover 📖	mathematical	Set.iUnion Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv chartAt Set.univ	SecondCountableTopology	—	TopologicalSpace.secondCountableTopology_of_countable_cover Encodable.countable OpenPartialHomeomorph.secondCountableTopology_source OpenPartialHomeomorph.open_source Set.biUnion_eq_iUnion
secondCountable_of_sigmaCompact 📖	mathematical	—	SecondCountableTopology	—	countable_cover_nhds_of_sigmaCompact chart_source_mem_nhds secondCountable_of_countable_cover
sum_chartAt_inl 📖	mathematical	—	chartAt instTopologicalSpaceSum sum OpenPartialHomeomorph.lift_openEmbedding nonempty_of_chartedSpace Topology.IsOpenEmbedding.inl	—	nonempty_of_chartedSpace Topology.IsOpenEmbedding.inl instIsEmptySum
sum_chartAt_inr 📖	mathematical	—	chartAt instTopologicalSpaceSum sum OpenPartialHomeomorph.lift_openEmbedding nonempty_of_chartedSpace Topology.IsOpenEmbedding.inr	—	nonempty_of_chartedSpace Topology.IsOpenEmbedding.inr instIsEmptySum
t1Space 📖	mathematical	—	T1Space	—	t1Space_iff_exists_open OpenPartialHomeomorph.isOpen_inter_preimage isOpen_compl_singleton Set.InjOn.ne OpenPartialHomeomorph.injOn mem_chart_source OpenPartialHomeomorph.open_source

ChartedSpaceCore

Definitions

Name	Category	Theorems
atlas 📖	CompOp	1 math math: chart_mem_atlas
chartAt 📖	CompOp	2 math math: chart_mem_atlas, mem_chart_source
openPartialHomeomorph 📖	CompOp	—
toChartedSpace 📖	CompOp	—
toTopologicalSpace 📖	CompOp	1 math math: open_source'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
chart_mem_atlas 📖	mathematical	—	PartialEquiv Set Set.instMembership atlas chartAt	—	—
continuousOn_toFun 📖	mathematical	PartialEquiv Set Set.instMembership atlas	ContinuousOn PartialEquiv.toFun PartialEquiv.trans PartialEquiv.symm PartialEquiv.source	—	—
mem_chart_source 📖	mathematical	—	Set Set.instMembership PartialEquiv.source chartAt	—	—
open_source 📖	mathematical	PartialEquiv Set Set.instMembership atlas	IsOpen PartialEquiv.source PartialEquiv.trans PartialEquiv.symm	—	—
open_source' 📖	mathematical	PartialEquiv Set Set.instMembership atlas	IsOpen toTopologicalSpace PartialEquiv.source	—	isOpen_univ Set.univ_inter
open_target 📖	mathematical	PartialEquiv Set Set.instMembership atlas	IsOpen PartialEquiv.target	—	Set.Subset.antisymm Set.inter_subset_left PartialEquiv.target_subset_preimage_source open_source

LibraryNote

Definitions

Name	Category	Theorems
Manifold_type_tags 📖	CompOp	—

ModelProd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	—	—	—	—
ext_iff 📖	—	—	—	—	ext

(root)

Definitions

Name	Category	Theorems
ChartedSpace 📖	CompData	—
ChartedSpaceCore 📖	CompData	—
ModelPi 📖	CompOp	1 math math: piChartedSpace_chartAt
ModelProd 📖	CompOp	355 math math: TangentBundle.tangentMap_tangentBundle_pure, contMDiff_prod_assoc, mfderiv_prod_eq_add, Prod.instLieGroup, Bundle.ContMDiffRiemannianMetric.contMDiff, Bundle.mdifferentiableAt_proj, mdifferentiableAt_sub_section, ContMDiffMul.prod, MDifferentiableOn.finsum_section_of_locallyFinite, ModelWithCorners.range_prod, Bundle.contMDiffOn_zeroSection, MDifferentiableAt.clm_bundle_apply, MDifferentiableAt.mfderiv_prod, mdifferentiableWithinAt_totalSpace, contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt, ContMDiffOn.prodMk, tangentMapWithin_prodSnd, ContMDiffOn.mlieBracketWithin_vectorField, ContMDiffWithinAt.mlieBracketWithin_vectorField, mdifferentiableAt_iff_localFrame_coeff, Bundle.Trivialization.contMDiffOn_section_baseSet_iff, MDifferentiableOn.smul_const_section, tangentMap_chart, ContMDiffWithinAt.sub_section, Manifold.IsImmersionOfComplement.prodMap, contMDiff_addInvariantVectorField, mdifferentiableWithinAt_smul_const_section, TangentBundle.coe_chartAt_fst, mdifferentiableAt_add_section, HasMFDerivWithinAt.prodMk, ContMDiffAt.finsum_section_of_locallyFinite, ContMDiffAdd.prod, ContMDiffMul.contMDiff_mul, Bundle.contMDiffWithinAt_zeroSection, mdifferentiableOn_snd, contMDiff_mul, contMDiff_mulInvariantVectorField, contMDiffWithinAt_snd, Bundle.Trivialization.contMDiffOn, contMDiffWithinAt_prod_iff, UniqueMDiffOn.prod, MDifferentiableWithinAt.finsum_section_of_locallyFinite, IsLocalFrameOn.contMDiffAt_of_coeff, contMDiff_equivTangentBundleProd_symm, mdifferentiableWithinAt_section, contMDiffOn_baseSet_iff_localFrame_coeff, ContMDiffWithinAt.add_section, ContMDiffAt.add_section, ContMDiffAdd.contMDiff_add, Manifold.IsSmoothEmbedding.prodMap, MDifferentiable.clm_bundle_apply₂, Manifold.IsImmersionAtOfComplement.prodMap, Diffeomorph.coe_prodCongr, tangentBundle_model_space_coe_chartAt, hasMFDerivAt_fst, writtenInExtChart_prod, Bundle.contMDiffAt_zeroSection, ModelWithCorners.prod_target, contMDiffAt_mulInvariantVectorField, MDifferentiable.prodMap, equivTangentBundleProd_apply, MDifferentiable.clm_bundle_apply, MDifferentiableWithinAt.clm_bundle_apply₂, HasMFDerivWithinAt.prodMap, mdifferentiableAt_addInvariantVectorField, ContMDiff.sum_section_of_locallyFinite, ContMDiff.contMDiff_tangentMap, MDifferentiableAt.mpullback_vectorField, ContMDiffWithinAt.sum_section, MDifferentiableAt.sum_section, mdifferentiableAt_fst, Bundle.Trivialization.mdifferentiableAt_section_iff, MDifferentiableOn.prodMk, mfderiv_prod_eq_add_comp, MDifferentiableAt.prodMap', ContMDiffAt.prodMap, mdifferentiableAt_totalSpace, mdifferentiableOn_fst, mdifferentiable_mulInvariantVectorField, FiberBundle.chartedSpace_chartAt, ContMDiffOn.finsum_section_of_locallyFinite, MDifferentiableOn.sum_section_of_locallyFinite, MDifferentiableAt.prodMk, ContMDiffWithinAt.neg_section, Diffeomorph.prodCongr_symm, ContMDiffWithinAt.mpullbackWithin_vectorField_inter, mdifferentiableAt_hom_bundle, IsLocalFrameOn.mdifferentiableAt_of_coeff_aux, mdifferentiable_fst, mdifferentiableWithinAt_neg_section, modelWithCorners_prod_coe, Bundle.TotalSpace.isManifold, ContMDiffAt.const_smul_section, contMDiff_vectorSpace_iff_contDiff, mdifferentiableAt_snd, ContMDiffOn.mpullbackWithin_vectorField_inter, mfderiv_prodMap, ContMDiffAt.clm_apply_of_inCoordinates, Bundle.Trivialization.mdifferentiableWithinAt_totalSpace_iff, MDifferentiable.mpullback_vectorField, mdifferentiable_smul_const_section, Bundle.Trivialization.mdifferentiableOn_section_baseSet_iff, UniqueMDiffWithinAt.bundle_preimage', FiberBundle.exists_contMDiffOn_extend, MDifferentiableAt.finsum_section_of_locallyFinite, IsContMDiffRiemannianBundle.exists_contMDiff, ModelWithCorners.prod_symm_apply, contMDiff_snd, ContMDiffAt.clm_bundle_apply, contMDiffAt_prod_iff, tangentMap_prodSnd, mdifferentiableAt_neg_section, Bundle.Trivialization.contMDiffOn_localFrame_baseSet, HasMFDerivAt.prodMap, MDifferentiableAt.clm_bundle_apply₂, ContMDiffWithinAt.mpullback_vectorField_of_mem_nhdsWithin_of_eq, FiberBundle.writtenInExtChartAt_trivializationAt, IsLocalFrameOn.mdifferentiableOn_of_coeff, ModelWithCorners.prod_source, ContMDiffWithinAt.mpullback_vectorField_preimage, hasMFDerivWithinAt_fst, MDifferentiableWithinAt.mpullbackWithin_vectorField_inter_of_eq, MDifferentiableOn.prodMap, MDifferentiableAt.smul_section, ContMDiffWithinAt.mpullback_vectorField_preimage_of_eq, FiberBundle.mdifferentiableAt_extend, modelWithCorners_prod_coe_symm, contMDiff_smul, MDifferentiableWithinAt.clm_apply_of_inCoordinates, prodChartedSpace_chartAt, Bundle.mdifferentiableWithinAt_proj, IsLocalFrameOn.contMDiffOn, MDifferentiableOn.clm_bundle_apply, MDifferentiableWithinAt.prodMk, Bundle.Trivialization.mdifferentiableOn_section_iff, tangentMapWithin_prodFst, ContMDiffWithinAt.finsum_section_of_locallyFinite, Bundle.contMDiffWithinAt_totalSpace, Diffeomorph.coe_prodComm, Bundle.Trivialization.contMDiffWithinAt_iff, mdifferentiableWithinAt_sub_section, Bundle.mdifferentiableOn_proj, mdifferentiableWithinAt_add_section, ContMDiffWithinAt.mpullbackWithin_vectorField', tangentBundle_model_space_coe_chartAt_symm, tangentBundleModelSpaceHomeomorph_coe, equivTangentBundleProd_symm_apply_snd, MDifferentiable.sum_section, ContMDiffWithinAt.clm_bundle_apply₂, TangentBundle.chartAt, IsLocalFrameOn.contMDiffAt, contMDiffAt_hom_bundle, ContMDiffOn.prodMap, MDifferentiable.sum_section_of_locallyFinite, ContMDiffRing.contMDiff_mul, contMDiff_prod_iff, FiberBundle.extChartAt, MDifferentiableWithinAt.sum_section_of_locallyFinite, ContMDiffAt.mlieBracket_vectorField, ContMDiffOn.add_section, mfderiv_prod_right, writtenInExtChartAt_prod, ContMDiff.finsum_section_of_locallyFinite, Bundle.contMDiffWithinAt_proj, ModelWithCorners.boundary_of_boundaryless_left, Bundle.contMDiffAt_totalSpace, MDifferentiableAt.clm_apply_of_inCoordinates, ContMDiffWithinAt.clm_bundle_apply, ContMDiff.clm_bundle_apply, UniqueMDiffOn.tangentBundle_proj_preimage, tangentBundle_model_space_chartAt, TangentBundle.mem_chart_target_iff, ContMDiff.clm_bundle_apply₂, mdifferentiable_snd, MDifferentiableOn.sum_section, mdifferentiableAt_prod_iff, MDifferentiable.prodMk, FiberBundle.contMDiffAt_extend', contMDiffWithinAt_fst, Bundle.contMDiffOn_proj, ContMDiffWithinAt.prodMk, Bundle.contMDiff_proj, contMDiffOn_fst, MDifferentiableAt.sum_section_of_locallyFinite, MDifferentiableOn.mpullback_vectorField_preimage, contMDiffOn_prod_iff, ContMDiffWithinAt.mpullbackWithin_vectorField_of_mem_of_eq, Manifold.IsImmersionAt.prodMap, IsManifold.prod, mfderivWithin_prodMap, tangentMap_chart_symm, UniqueMDiffWithinAt.bundle_preimage, contMDiffAt_vectorSpace_iff_contDiffAt, ContMDiff.neg_section, Manifold.IsImmersion.prodMap, Bundle.mdifferentiableWithinAt_zeroSection, mfderiv_snd, mdifferentiable_addInvariantVectorField, VectorField.contMDiffWithinAt_mpullbackWithin_extChartAt_symm, modelWithCorners_prod_toPartialEquiv, Bundle.Trivialization.contMDiff_iff, ContMDiffWithinAt.sum_section_of_locallyFinite, Bundle.contMDiff_zeroSection, ContDiff.mlieBracket_vectorField, FiberBundle.extChartAt_target, contMDiffAt_localFrame_of_mem, mdifferentiableWithinAt_snd, mfderiv_prodMk, hasMFDerivWithinAt_snd, mdifferentiableAt_section, Bundle.Trivialization.contMDiffAt_section_iff, Bundle.mdifferentiable_proj, ContMDiffWithinAt.clm_apply_of_inCoordinates, FiberBundle.writtenInExtChartAt_trivializationAt_symm, ModelWithCorners.boundary_of_boundaryless_right, ContMDiffAt.sub_section, ModelWithCorners.range_eq_univ_prod, ModelWithCorners.prod_apply, tangentBundleModelSpaceHomeomorph_coe_symm, MDifferentiableWithinAt.mpullback_vectorField_preimage, MDifferentiableWithinAt.clm_bundle_apply, ContMDiffSection.contMDiff, IsManifold.mem_maximalAtlas_prod, contMDiff_equivTangentBundleProd, UniqueMDiffOn.bundle_preimage, Bundle.Trivialization.contMDiffAt_iff, ContMDiffOn.const_smul_section, Bundle.contMDiffAt_section, Bundle.Trivialization.contMDiffWithinAt_section, ModelWithCorners.boundary_prod, MDifferentiableOn.mpullbackWithin_vectorField_inter, ContMDiffAt.clm_bundle_apply₂, ContMDiffWithinAt.mpullbackWithin_vectorField_inter_of_eq, mDifferentiableOn_sub_section, equivTangentBundleProd_eq_tangentMap_prod_tangentMap, mdifferentiable_prod_iff, mdifferentiableOn_prod_iff, Bundle.Trivialization.contMDiffOn_symm, mdifferentiableAt_mulInvariantVectorField, mfderivWithin_prodMk, contMDiffAt_iff_localFrame_coeff, modelProd_range_prod_id, ContMDiffOn.sum_section_of_locallyFinite, ContMDiffAt.prodMap', tangentMap_prodFst, ContMDiffCovariantDerivativeOn.contMDiff, MDifferentiableWithinAt.mpullbackWithin_vectorField_inter, ContMDiffOn.contMDiffOn_tangentMapWithin, mdifferentiable_sub_section, ContMDiffWithinAt.const_smul_section, mdifferentiable_neg_section, ContMDiffWithinAt.prodMap', ContMDiffAt.sum_section_of_locallyFinite, mdifferentiableWithinAt_fst, MDifferentiable.finsum_section_of_locallyFinite, ContMDiffOn.mpullback_vectorField_preimage, IsLocalFrameOn.contMDiffOn_of_coeff, ModelWithCorners.BoundarylessManifold.prod, contMDiff_add, FiberBundle.exists_mdifferentiableOn_extend, Diffeomorph.prodComm_symm, Prod.instLieAddGroup, HasMFDerivAt.prodMk, ContMDiff.sub_section, MDifferentiableWithinAt.mpullback_vectorField_preimage_of_eq, ContMDiffWithinAt.mpullbackWithin_vectorField, ContMDiffAt.prodMk, Bundle.contMDiffAt_proj, contMDiffAt_addInvariantVectorField, contMDiff_tangentBundleModelSpaceHomeomorph, MDifferentiableAt.smul_const_section, ContMDiffAt.mpullback_vectorField_preimage, ContMDiffOn.smul_section_of_tsupport, ContMDiffWithinAt.smul_section, mdifferentiable_add_section, hasMFDerivAt_snd, hom_chart, MDifferentiableOn.smul_section, MDifferentiableWithinAt.prodMap, TangentBundle.coe_chartAt_symm_fst, Bundle.contMDiffWithinAt_section, Bundle.mdifferentiableOn_zeroSection, ContMDiffSection.mdifferentiable', contMDiff_tangentBundleModelSpaceHomeomorph_symm, mfderiv_fst, mfderivWithin_fst, ContMDiffWithinAt.mpullbackWithin_vectorField_of_eq, ContMDiffOn.sub_section, ContMDiffSection.mdifferentiableAt, MDifferentiableOn.smul_section_of_tsupport, ContMDiff.add_section, ContMDiffOn.sum_section, ContMDiffOn.neg_section, UniqueMDiffWithinAt.prod, equivTangentBundleProd_symm_apply_proj, ContMDiffSection.mdifferentiable, Bundle.Trivialization.contMDiffOn_iff, ContMDiffWithinAt.prodMap, mdifferentiable_smul_section, Bundle.mdifferentiable_zeroSection, Bundle.Trivialization.mdifferentiableWithinAt_section_iff, contMDiffAt_fst, mdifferentiableWithinAt_prod_iff, ContMDiffWithinAt.mpullbackWithin_vectorField_of_mem, VectorField.eventually_contMDiffWithinAt_mpullbackWithin_extChartAt_symm, IsLocalFrameOn.mdifferentiableAt_of_coeff, TangentBundle.chartAt_toPartialEquiv, ContMDiffAt.sum_section, ContMDiff.const_smul_section, tangentMap_prod_right, contMDiffOn_vectorSpace_iff_contDiffOn, ContMDiffOn.clm_bundle_apply, Bundle.Trivialization.contMDiffOn_section_iff, tangentMap_prod_left, mdifferentiableOn_add_section, FiberBundle.chartedSpace_chartAt_symm_fst, ContMDiffSection.contMDiff_toFun, ContMDiffAt.smul_section, contDiffGroupoid_prod, ModelWithCorners.interior_prod, contMDiffOn_snd, mfderiv_prod_left, ContMDiffAt.neg_section, MDifferentiableWithinAt.prodMap', mdifferentiableWithinAt_hom_bundle, IsLocalFrameOn.contMDiffAt_of_coeff_aux, Bundle.Trivialization.contMDiffOn_symm_trans, contMDiff_fst, Bundle.mdifferentiableAt_zeroSection, boundary_product, MDifferentiableAt.prodMap, ContMDiff.sum_section, mdifferentiableOn_neg_section, Bundle.Trivialization.mdifferentiableAt_totalSpace_iff, ContMDiff.prodMap, contMDiff_snd_tangentBundle_modelSpace, ContMDiffWithinAt.mpullbackWithin_vectorField_of_eq', contMDiffWithinAt_hom_bundle, mfderivWithin_snd, MDifferentiableOn.clm_bundle_apply₂, contMDiffAt_snd, ContMDiffOn.clm_bundle_apply₂, mfderiv_prod_eq_add_apply, extChartAt_prod, ContMDiff.mpullback_vectorField, Bundle.Trivialization.Bundle.Trivialization.mdifferentiable, TangentBundle.mem_chart_source_iff, MDifferentiableWithinAt.sum_section, ContMDiff.smul_section, ContMDiffWithinAt.mpullback_vectorField_of_mem_nhdsWithin, Manifold.LiftSourceTargetPropertyAt.prodMap, MDifferentiableWithinAt.smul_section, ContMDiffOn.smul_section, contMDiffOn_iff_localFrame_coeff, ContMDiff.prodMk
achart 📖	CompOp	14 math math: TangentBundle.symmL_trivializationAt_eq_core, TangentBundle.continuousLinearMapAt_trivializationAt_eq_core, coe_achart, TangentBundle.coordChange_model_space, inTangentCoordinates_eq, TangentBundle.chartAt, tangentBundleCore_coordChange_model_space, mem_achart_source, achart_val, TangentBundle.trivializationAt_eq_localTriv, TangentBundle.chartAt_toPartialEquiv, achart_def, tangentBundleCore_indexAt, tangentBundleCore_coordChange_achart
atlas 📖	CompOp	24 math math: TangentBundle.symmL_trivializationAt_eq_core, TangentBundle.continuousLinearMapAt_trivializationAt_eq_core, coe_achart, TangentBundle.coordChange_model_space, inTangentCoordinates_eq, chartedSpaceSelf_atlas, TangentBundle.chartAt, tangentBundleCore_coordChange_model_space, chart_mem_atlas, tangentBundleCore_coordChange, mem_achart_source, contDiffOn_fderiv_coord_change, tangentBundleCore.isContMDiff, achart_val, StructureGroupoid.subset_maximalAtlas, TangentBundle.trivializationAt_eq_localTriv, tangentBundleCore_baseSet, tangentBundleCore_localTriv_baseSet, IsManifold.subset_maximalAtlas, TangentBundle.chartAt_toPartialEquiv, achart_def, tangentBundleCore_indexAt, tangentBundleCore_coordChange_achart, ChartedSpace.mem_atlas_sum
chartAt 📖	CompOp	95 math math: ChartedSpace.sum_chartAt_inr, SmoothPartitionOfUnity.exists_isSubordinate_chartAt_source, writtenInExtChartAt_chartAt, TopologicalSpace.Opens.chartAt_eq, contMDiffOn_chart, chart_target_mem_nhds, tangentMap_chart, TopologicalSpace.Opens.chartAt_subtype_val_symm_eventuallyEq, StructureGroupoid.LocalInvariantProp.liftPropAt_chart_symm, mem_chart_source, mdifferentiableOn_extChartAt, TangentBundle.coe_chartAt_fst, ChartedSpace.LiftPropWithinAt.prop, hasMFDerivAt_extChartAt, mdifferentiable_chart, contMDiffOn_chart_symm, chart_source_mem_nhds, SmoothBumpFunction.exists_r_pos_lt_subset_ball, tangentBundle_model_space_coe_chartAt, coe_achart, TopologicalSpace.Opens.chart_eq', chartedSpace_of_discreteTopology_chartAt, Icc_chartedSpaceChartAt_of_le_top, TopologicalSpace.Opens.chartAt_inclusion_symm_eventuallyEq, iUnion_source_chartAt, hasMFDerivWithinAt_extChartAt, FiberBundle.chartedSpace_chartAt, StructureGroupoid.chart_mem_maximalAtlas, SmoothBumpFunction.support_eq_inter_preimage, mfderiv_chartAt_eq_tangentCoordChange, TangentBundle.trivializationAt_apply, TopologicalSpace.Opens.chart_eq, ChartedSpace.sum_chartAt_inl, Icc_chartedSpaceChartAt, SmoothBumpFunction.tsupport_subset_chartAt_source, ChartedSpace.liftPropAt_iff, SmoothBumpFunction.eqOn_source, contMDiffOn_extChartAt, isOpen_extChartAt_preimage, prodChartedSpace_chartAt, extChartAt_source, FiberBundle.chartedSpace'_chartAt, ChartedSpace.liftProp_iff, IsManifold.chart_mem_maximalAtlas, TangentBundle.trivializationAt_source, ext_coord_change_source, StructureGroupoid.liftPropWithinAt_self_target, tangentBundle_model_space_coe_chartAt_symm, SmoothBumpCovering.mem_chartAt_ind_source, TangentBundle.chartAt, chart_mem_atlas, writtenInExtChartAt_chartAt_comp, tangentBundle_model_space_chartAt, TangentBundle.mem_chart_target_iff, ChartedSpace.isOpen_iff, SmoothPartitionOfUnity.exists_isSubordinate_chartAt_source_of_isClosed, Icc_chartedSpaceChartAt_of_top_le, achart_val, tangentMap_chart_symm, StructureGroupoid.LocalInvariantProp.liftPropOn_chart, SmoothBumpCovering.comp_embeddingPiTangent_mfderiv, SmoothBumpFunction.coe_def, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_iff, writtenInExtChartAt_sumSwap_eventuallyEq_id, chartAt_comp, TangentBundle.trivializationAt_baseSet, writtenInExtChartAt_chartAt_symm_comp, writtenInExtChartAt_chartAt_symm, extChartAt_target, hom_chart, TangentBundle.coe_chartAt_symm_fst, extChartAt_coe_symm, extChartAt_comp, StructureGroupoid.liftPropWithinAt_self_source, SmoothBumpFunction.support_subset_source, OpenPartialHomeomorph.singletonChartedSpace_chartAt_eq, TangentBundle.chartAt_toPartialEquiv, StructureGroupoid.LocalInvariantProp.liftPropOn_chart_symm, mem_chart_target, Units.chartAt_source, FiberBundle.chartedSpace_chartAt_symm_fst, piChartedSpace_chartAt, StructureGroupoid.LocalInvariantProp.liftPropAt_chart, OpenPartialHomeomorph.singletonChartedSpace_chartAt_source, sum_chartAt_inl_apply, extChartAt_coe, achart_def, SmoothBumpCovering.mem_chartAt_source_of_eq_one, Topology.IsOpenEmbedding.singletonChartedSpace_chartAt_eq, TangentBundle.mem_chart_source_iff, chartAt_self_eq, TangentBundle.trivializationAt_target, Units.chartAt_apply, sum_chartAt_inr_apply, ChartedSpace.liftPropWithinAt_iff'
chartedSpaceSelf 📖	CompOp	613 math math: TangentBundle.continuousLinearMapAt_model_space, ContMDiffAt.coordChangeL, MDifferentiable.coordChangeL, UpperHalfPlane.mdifferentiable_num, HasMFDerivAt.mul, SmoothBumpCovering.toSmoothPartitionOfUnity_eq_mul_prod, LeftInvariantDerivation.lift_zero, MDifferentiable.add, exists_contMDiffMap_zero_one_of_isClosed, MDifferentiableOn.clm_postcomp, contMDiffAt_extend, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart', CuspFormClass.holo, HasMFDerivAt.add, DifferentiableWithinAt.comp_mdifferentiableWithinAt, LeftInvariantDerivation.leibniz, contMDiffWithinAt_iff_target, writtenInExtChartAt_chartAt, ContMDiffMap.coeFnAlgHom_apply, mfderivWithin_range_extChartAt_symm, MDifferentiableAt.prod, Manifold.pathELength_eq_lintegral_mfderiv_Ioo, MDifferentiableWithinAt.add, ContDiffWithinAt.contMDiffWithinAt, MDifferentiableAt.cle_arrowCongr, mdifferentiableWithinAt_totalSpace, contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt, smoothSheafCommRing.nonunits_stalk, MDifferentiableWithinAt.differentiableWithinAt_mpullbackWithin_vectorField, mdifferentiableAt_iff_localFrame_coeff, contMDiffOn_chart, Bundle.Trivialization.contMDiffOn_section_baseSet_iff, ContDiffAt.contMDiffAt, MDifferentiableAt.sum, mdifferentiable_iff_target, contMDiffAt_iff_source, SmoothPartitionOfUnity.contMDiffAt_finsum, MDifferentiableOn.prodMk_space, ContinuousLinearEquiv.symm_toDiffeomorph, eventually_enorm_mfderivWithin_symm_extChartAt_lt, tangentMap_chart, StructureGroupoid.LocalInvariantProp.liftPropAt_chart_symm, LeftInvariantDerivation.coe_derivation, TangentBundle.symmL_trivializationAt, SmoothPartitionOfUnity.locallyFinite, exists_smooth_one_nhds_of_subset_interior, ContMDiffWithinAt.mfderivWithin_const, ContMDiffOn.clm_postcomp, SmoothPartitionOfUnity.nonneg, LeftInvariantDerivation.left_invariant', chartedSpaceSelf_prod, MDifferentiableWithinAt.mul, mdifferentiableOn_extChartAt, mdifferentiableOn_symm_coordChangeL, SmoothBumpCovering.exists_immersion_euclidean, IsOpen.exists_msmooth_support_eq, SmoothPartitionOfUnity.locallyFinite', ContMDiff.clm_apply, ModelWithCorners.mdifferentiableOn_symm, ContinuousLinearEquiv.coe_toDiffeomorph_symm, VectorField.mlieBracket_smul_left, Bundle.Trivialization.contMDiffOn, MDifferentiable.sum, hasMFDerivAt_extChartAt, ContinuousLinearMap.contMDiff, ContinuousLinearMap.mdifferentiable, instContMDiffAddSelf, mdifferentiable_chart, ContMDiffAt.clm_postcomp, ContMDiffWithinAt.clm_postcomp, smoothSheafCommRing.instLocalRing_stalk, MDifferentiable.smul, Differentiable.comp_mdifferentiableAt, mdifferentiableWithinAt_section, contMDiffOn_localFrame_coeff, OpenPartialHomeomorph.contMDiffOn_writtenInExtend_iff, VectorBundleCore.contMDiffOn_coordChange, MDifferentiable.clm_postcomp, contMDiffOn_chart_symm, MDifferentiableWithinAt.prodMk_space, contMDiffOn_baseSet_iff_localFrame_coeff, ContMDiffWithinAt.coordChange, inTangentCoordinates_eq_mfderiv_comp, ContMDiff.coordChange, mfderivWithin_projIcc_one, MDifferentiable.cle_arrowCongr, ContMDiffAt.mfderiv_apply, LeftInvariantDerivation.lift_add, contMDiffOn_isOpenEmbedding_symm, StructureGroupoid.mem_maximalAtlas_of_mem_groupoid, tangentBundle_model_space_coe_chartAt, StructureGroupoid.LocalInvariantProp.liftPropAt_of_mem_groupoid, ContMDiff.smul, contMDiffOn_iff_contDiffOn, MDifferentiable.const_smul, mfderivWithin_comp_projIcc_one, UpperHalfPlane.mdifferentiable_inv_denom, LeftInvariantDerivation.lift_smul, TopologicalSpace.Opens.chart_eq', MDifferentiableAt.mul, SmoothPartitionOfUnity.sum_finsupport', HasMFDerivAt.smul, MDifferentiableOn.smul, MDifferentiableAt.clm_prodMap, HasMFDerivAt.neg, Manifold.pathELength_def, MDifferentiableAt.pow, fromTangentSpace_mfderiv_smul_apply, contMDiffWithinAt_prod_module_iff, MDifferentiableAt.clm_postcomp, ModelWithCorners.hasMFDerivAt, instNormedSpaceLieAddGroup, eventually_norm_mfderivWithin_symm_extChartAt_lt, VectorField.mpullback_eq_pullback, MDifferentiableAt.add, ContMDiff.piecewise_Iic, HasMFDerivWithinAt.neg, UpperHalfPlane.contMDiff_coe, CuspForm.holo', contMDiff_coe_sphere, ContDiffAt.comp_contMDiffWithinAt, LeftInvariantDerivation.comp_L, IsOpen.exists_contMDiff_support_eq_aux, MDifferentiableWithinAt.coordChange, extChartAt_self_apply, Manifold.pathELength_eq_lintegral_mfderivWithin_Icc, hasMFDerivAt_neg, ContinuousLinearEquiv.hasMFDerivAt, SmoothBumpCovering.toSmoothPartitionOfUnity_apply, SmoothPartitionOfUnity.contDiffAt_finsum, ContMDiffAt.smul, Bundle.Trivialization.mdifferentiableAt_section_iff, mdifferentiableOn_iff_target, contMDiff_isOpenEmbedding, contMDiff_model, ContinuousLinearEquiv.hasMFDerivWithinAt, ContDiffOn.contMDiffOn, UpperHalfPlane.contMDiff_inv_denom, hasMFDerivWithinAt_extChartAt, contMDiffWithinAt_pi_space, ContMDiffFiberwiseLinear.locality_aux₂, BumpCovering.contMDiff_toPartitionOfUnity, MDifferentiableWithinAt.cle_arrowCongr, MDifferentiableWithinAt.clm_precomp, mdifferentiableAt_totalSpace, UniqueMDiffOn.uniqueMDiffOn_target_inter, mdifferentiableOn_prod_module_iff, contMDiffAt_iff_source_of_mem_source, Metric.exists_smooth_forall_closedBall_subset, mdifferentiableOn_localFrame_coeff, mfderiv_chartAt_eq_tangentCoordChange, DifferentiableWithinAt.mdifferentiableWithinAt, LeftInvariantDerivation.evalAt_coe, ContMDiffOn.clm_precomp, ContMDiffOn.coordChangeL, mfderivWithin_extChartAt_symm_inverse_apply, mdifferentiableAt_hom_bundle, SmoothPartitionOfUnity.le_one, MDifferentiable.coordChange, mfderiv_sub, Continuous.exists_contMDiff_approx, exists_contMDiffMap_zero_one_nhds_of_isClosed, contMDiffOn_pi_space, UniqueDiffWithinAt.uniqueMDiffWithinAt, ContMDiffAt.mfderiv_const, smoothSheafCommRing.isUnit_stalk_iff, contMDiff_vectorSpace_iff_contDiff, ContMDiffWithinAt.change_section_trivialization, LeftInvariantDerivation.map_zero, ContDiff.comp_contMDiff, TangentBundle.coordChange_model_space, ContMDiffWithinAt.prodMk_space, Bundle.Trivialization.mdifferentiableWithinAt_totalSpace_iff, fdifferential_apply, HasFDerivAt.hasMFDerivAt, SmoothBumpFunction.contMDiffAt, Bundle.Trivialization.mdifferentiableOn_section_baseSet_iff, MDifferentiableOn.coordChangeL, mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm, ContMDiffMap.smul_comp, DifferentiableAt.comp_mdifferentiableWithinAt, ContMDiffOn.cle_arrowCongr, MDifferentiableAt.const_smul, SmoothBumpCovering.sum_toSmoothPartitionOfUnity_eq, MDifferentiableOn.clm_prodMap, contMDiffAt_coordChangeL, contMDiff_subtype_coe_Icc, LeftInvariantDerivation.coe_sub, MDifferentiableWithinAt.coordChangeL, ContMDiffAt.prodMk_space, extChartAt_self_eq, FiberBundle.writtenInExtChartAt_trivializationAt, LeftInvariantDerivation.left_invariant'', contMDiff_iff_contDiff, contMDiff_iff_target, ContMDiffOn.clm_comp, ContDiff.comp_contMDiffWithinAt, mdifferentiableOn_extChartAt_symm, fromTangentSpace_mfderiv_smul', UpperHalfPlane.contMDiff_num, SmoothPartitionOfUnity.sum_eq_one', MDifferentiableOn.add, VectorField.mlieBracketWithin_def, UpperHalfPlane.mdifferentiable_denom, mdifferentiableAt_prod_module_iff, writtenInExtChartAt_model_space, contMDiffOn_extChartAt, MDifferentiableOn.prod, HasMFDerivWithinAt.hasFDerivWithinAt, contMDiffOn_baseSet_localFrame_coeff, SmoothPartitionOfUnity.mem_finsupport, IsOpen.exists_contMDiff_support_eq, fromTangentSpace_mfderiv_smul_apply', DifferentiableOn.mdifferentiableOn, ContinuousLinearEquiv.mdifferentiableOn, mdifferentiableWithinAt_iff_differentiableWithinAt, MDifferentiable.prodMk_space, contMDiff_smul, trivializationAt_model_space_apply, ContDiffAt.comp_contMDiffAt, contMDiffOn_continuousLinearMapCoordChange, mfderiv_coe_sphere_injective, contMDiffOn_extChartAt_symm, mfderiv_add, MDifferentiableAt.sub, chartedSpaceSelf_atlas, contMDiffWithinAt_extChartAt_symm_range_self, MDifferentiableAt.clm_comp, ContinuousLinearMap.mfderiv_eq, Bundle.Trivialization.mdifferentiableOn_section_iff, contMDiffWithinAt_iff_target_of_mem_source, Bundle.contMDiffWithinAt_totalSpace, MDifferentiable.slash, contMDiffWithinAt_iff_source_of_mem_maximalAtlas, mfderiv_extChartAt_self, ContMDiffWithinAt.smul, Bundle.Trivialization.contMDiffWithinAt_iff, IsMIntegralCurveAt.hasMFDerivAt, exists_contMDiffOn_forall_mem_convex_of_local, ContMDiffOn.prodMk_space, SmoothBumpCovering.embeddingPiTangent_injective_mfderiv, ModelWithCorners.mdifferentiableAt, VectorField.mlieBracketWithin_smul_left, StructureGroupoid.liftPropWithinAt_self_target, MDifferentiableOn.sum, exists_msmooth_support_eq_eq_one_iff, tangentBundle_model_space_coe_chartAt_symm, SmoothPartitionOfUnity.coe_finsupport, tangentBundleModelSpaceHomeomorph_coe, Emetric.exists_contMDiffMap_forall_closedBall_subset, contMDiffOn_of_mem_contDiffGroupoid, MDifferentiableOn.inner_bundle, Diffeomorph.contDiff, contMDiffOn_symm_coordChangeL, tangentBundleCore_coordChange_model_space, Metric.exists_contMDiffMap_forall_closedBall_subset, contMDiffAt_hom_bundle, VectorField.mlieBracketWithin_smul_right, exists_msmooth_zero_iff_one_iff_of_isClosed, LeftInvariantDerivation.map_add, MDifferentiableAt.coordChange, SmoothPartitionOfUnity.finsum_smul_mem_convex, mdifferentiableOn_baseSet_localFrame_coeff, LeftInvariantDerivation.coe_add, StructureGroupoid.LocalInvariantProp.liftPropOn_of_mem_groupoid, ContMDiffAt.clm_precomp, ContDiff.contMDiff, HasMFDerivWithinAt.sum, SmoothPartitionOfUnity.sum_le_one', MDifferentiable.clm_prodMap, instIsRiemannianManifoldModelWithCornersSelfReal, SmoothBumpCovering.embeddingPiTangent_ker_mfderiv, ContMDiffOn.inner_bundle, ModelWithCorners.hasMFDerivWithinAt, SmoothPartitionOfUnity.sum_nonneg, StructureGroupoid.LocalInvariantProp.liftPropOn_of_mem_maximalAtlas, contMDiffAt_localFrame_coeff, HasMFDerivWithinAt.mul', ContMDiffOn.clm_apply, Bundle.contMDiffAt_totalSpace, Diffeomorph.uniqueDiffOn_image, LeftInvariantDerivation.coe_injective, MDifferentiableWithinAt.inner_bundle, MDifferentiableAt.prodMk_space, HasFDerivWithinAt.hasMFDerivWithinAt, UpperHalfPlane.contMDiff_denom_zpow, SmoothBumpCovering.exists_finset_toSmoothPartitionOfUnity_eventuallyEq, ContinuousLinearMap.mdifferentiableWithinAt, LeftInvariantDerivation.coe_neg, TangentBundle.continuousLinearMapAt_trivializationAt, contMDiffWithinAt_comp_projIcc_iff, tangentBundle_model_space_chartAt, MDifferentiable.mul, mdifferentiableAt_iff_target_of_mem_source, MDifferentiableOn.cle_arrowCongr, MDifferentiableAt.smul, HasMFDerivAt.hasFDerivAt, ContMDiffWithinAt.mfderivWithin, IsOpen.exists_msmooth_support_eq_aux, ext_chart_model_space_apply, MDifferentiableOn.clm_apply, StructureGroupoid.liftPropWithinAt_self, MDifferentiableAt.clm_precomp, exists_contMDiff_zero_iff_one_iff_of_isClosed, writtenInExtChartAt_extChartAt, SmoothBumpFunction.contMDiff_smul, StructureGroupoid.LocalInvariantProp.liftPropAt_symm_of_mem_maximalAtlas, contMDiffAt_iff_target_of_mem_source, ContMDiffMap.coe_smul, ContinuousLinearMap.hasMFDerivAt, mdifferentiableOn_continuousLinearMapCoordChange, MDifferentiableAt.neg, mfderivWithin_eq_fderivWithin, VectorField.eventuallyEq_mpullback_mpullbackWithin_extChartAt, extChartAt_model_space_eq_id, eventually_enorm_mfderiv_extChartAt_lt, enorm_tangentSpace_vectorSpace, LeftInvariantDerivation.map_smul, oneTangentSpaceIcc_def, ModelWithCorners.uniqueMDiffOn, ModelWithCorners.hasMFDerivWithinAt_symm, SmoothPartitionOfUnity.sum_eq_one, fromTangentSpace_mfderiv_smul, mdifferentiableAt_neg, mdifferentiableOn_atlas, Differentiable.comp_mdifferentiable, instContMDiffInv₀ModelWithCornersSelf, contMDiffOn_iff_source_of_mem_maximalAtlas, SmoothBumpCovering.embeddingPiTangent_injOn, contMDiffWithinAt_extChartAt_symm_target_self, tangentMap_chart_symm, StructureGroupoid.LocalInvariantProp.liftPropOn_chart, HasMFDerivAt.sub, MDifferentiableWithinAt.clm_comp, contMDiffAt_vectorSpace_iff_contDiffAt, contMDiffWithinAt_iff_contDiffWithinAt, MDifferentiableOn.clm_comp, PointedContMDiffMap.instIsScalarTowerSomeENatTopContMDiffMapModelWithCornersSelf, LeftInvariantDerivation.coe_smul, HasMFDerivWithinAt.add, ContMDiffAt.clm_prodMap, ContMDiffWithinAt.mfderivWithin_apply, Continuous.exists_contMDiff_approx_and_eqOn, ContinuousLinearEquiv.mdifferentiableWithinAt, ContinuousLinearEquiv.mdifferentiable, writtenInExtChartAt_extChartAt_symm, mdifferentiableWithinAt_comp_projIcc_iff, exists_contMDiffMap_forall_mem_convex_of_local, ContinuousLinearMap.mfderivWithin_eq, VectorField.contMDiffWithinAt_mpullbackWithin_extChartAt_symm, mdifferentiableWithinAt_iff_source_of_mem_maximalAtlas, mdifferentiableOn_iff_differentiableOn, TangentBundle.symmL_model_space, Bundle.Trivialization.contMDiff_iff, Differentiable.mdifferentiable, range_mfderiv_coe_sphere, uniqueMDiffOn_iff_uniqueDiffOn, contMDiffAt_extChartAt, mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm', SmoothBumpCovering.comp_embeddingPiTangent_mfderiv, ContinuousLinearEquiv.mfderiv_eq, MDifferentiable.sub, mdifferentiableOn_coordChangeL, contMDiffAt_symm_of_mem_maximalAtlas, contMDiffWithinAt_extChartAt_symm_target, ContMDiffVectorBundle.contMDiffOn_coordChangeL, instIsManifoldModelSpace, contMDiff_prod_module_iff, VectorBundleCore.IsContMDiff.contMDiffOn_coordChange, mdifferentiableAt_section, mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt', Bundle.Trivialization.contMDiffAt_section_iff, SmoothPartitionOfUnity.exists_pos_of_mem, HasMFDerivAt.prod, FiberBundle.writtenInExtChartAt_trivializationAt_symm, ContMDiff.clm_postcomp, exists_smooth_zero_one_of_isClosed, ModelWithCorners.mdifferentiable, MDifferentiableAt.coordChangeL, ContMDiff.inner_bundle, tangentBundleModelSpaceHomeomorph_coe_symm, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_source, mdifferentiableAt_atlas_symm, MDifferentiableWithinAt.clm_postcomp, Derivative.normalizedDerivOfComplex_mdifferentiable, ContMDiff.clm_prodMap, mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt, Diffeomorph.uniqueDiffOn_preimage, SmoothBumpCovering.embeddingPiTangent_injective, exists_contMDiff_support_eq_eq_one_iff, ContMDiffAt.inner_bundle, LeftInvariantDerivation.map_sub, SmoothPartitionOfUnity.sum_finsupport_smul_eq_finsum, LeftInvariantDerivation.map_neg, Differentiable.comp_mdifferentiableWithinAt, Bundle.Trivialization.contMDiffAt_iff, contMDiffWithinAt_iff_source, SmoothPartitionOfUnity.contMDiff_finsum_smul, Bundle.contMDiffAt_section, MDifferentiableOn.clm_precomp, SmoothPartitionOfUnity.sum_finsupport, Bundle.Trivialization.contMDiffWithinAt_section, contMDiffWithinAt_iff_source_of_mem_source, MDifferentiableOn.coordChange, VectorField.mpullback_mfderivWithin_apply_smul, HasMFDerivWithinAt.mul, ContinuousLinearEquiv.coe_toDiffeomorph, VectorField.mfderiv_extChartAt_inverse_comp_mfderivWithin_extChartAT_symm, exists_smooth_forall_mem_convex_of_local_const, VectorField.mpullbackWithin_eq_pullbackWithin, Manifold.pathELength_eq_lintegral_mfderiv_Icc, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_target, norm_tangentSpace_vectorSpace, Bundle.Trivialization.contMDiffOn_symm, contMDiffAt_iff_localFrame_coeff, mdifferentiableAt_iff_source_of_mem_source, contMDiffAt_prod_module_iff, mdifferentiable_of_mem_atlas, mdifferentiable_jacobiTheta, ContMDiffWithinAt.clm_apply, SmoothBumpCovering.support_toSmoothPartitionOfUnity_subset, MDifferentiableOn.neg, contMDiffOn_of_mem_maximalAtlas, hasMFDerivAt_iff_hasFDerivAt, mdifferentiableAt_iff_differentiableAt, mdifferentiableWithinAt_iff_target_of_mem_source, mdifferentiableWithinAt_extChartAt_symm, contMDiffOn_comp_projIcc_iff, SmoothBumpFunction.contMDiff, ModelWithCorners.mdifferentiableOn, contMDiffWithinAt_extChartAt_symm_range, ContMDiffWithinAt.coordChangeL, UpperHalfPlane.contMDiffAt_ofComplex, eventually_norm_mfderivWithin_symm_extChartAt_comp_lt, ModularForm.holo', SmoothPartitionOfUnity.finite_tsupport, ContMDiffFiberwiseLinear.locality_aux₁, ContMDiffMap.smul_comp', ContMDiffAt.mfderiv, LeftInvariantDerivation.coe_zero, UpperHalfPlane.contMDiffAt_iff, contMDiffOn_extend_symm, exists_embedding_euclidean_of_compact, VectorPrebundle.contMDiffOn_contMDiffCoordChange, LeftInvariantDerivation.toDerivation_injective, ContinuousLinearMap.contMDiffWithinAt, mdifferentiableAt_coordChangeL, BumpCovering.coe_toSmoothPartitionOfUnity, ContMDiffOn.coordChange, writtenInExtChartAt_chartAt_symm, contMDiffAt_of_mem_maximalAtlas, mdifferentiableWithinAt_iff_source_of_mem_source, UpperHalfPlane.mdifferentiable_coe, MDifferentiableOn.mul, StructureGroupoid.LocalInvariantProp.liftPropOn_symm_of_mem_maximalAtlas, mfderiv_smul, Units.contMDiff_val, contMDiff_tangentBundleModelSpaceHomeomorph, ContMDiffWithinAt.clm_prodMap, SmoothPartitionOfUnity.mem_fintsupport_iff, Emetric.exists_smooth_forall_closedBall_subset, isInvertible_mfderiv_extChartAt, OpenPartialHomeomorph.contMDiffWithinAt_writtenInExtend_iff, ModularFormClass.holo, mdifferentiableWithinAt_prod_module_iff, mdifferentiableAt_iff_target, contMDiff_pi_space, contMDiffAt_extChartAt', uniqueMDiffWithinAt_iff_uniqueDiffWithinAt, MDifferentiable.clm_apply, HasMFDerivAt.sum, DifferentiableWithinAt.mdifferentiableWithinAt_of_comp_extChartAt_symm, ContMDiffAt.clm_apply, MDifferentiable.clm_precomp, ContinuousLinearMap.hasMFDerivWithinAt, Bundle.contMDiffWithinAt_section, MDifferentiable.clm_comp, ContMDiff.clm_comp, VectorPrebundle.IsContMDiff.exists_contMDiffCoordChange, contMDiff_tangentBundleModelSpaceHomeomorph_symm, ContinuousLinearMap.contMDiffOn, StructureGroupoid.liftPropWithinAt_self_source, contMDiffOn_coordChangeL, contMDiffOn_model_symm, nnnorm_tangentSpace_vectorSpace, mfderiv_eq_fderiv, MDifferentiableAt.inner_bundle, ContMDiffWithinAt.clm_precomp, exists_smooth_forall_mem_convex_of_local, EisensteinSeries.eisensteinSeries_SIF_MDifferentiable, ContinuousLinearMap.mdifferentiableOn, StructureGroupoid.LocalInvariantProp.liftPropAt_of_mem_maximalAtlas, ContMDiff.clm_precomp, LeftInvariantDerivation.commutator_apply, UpperHalfPlane.mdifferentiableAt_iff, ContMDiffOn.clm_prodMap, LeftInvariantDerivation.commutator_coe_derivation, ContMDiffWithinAt.clm_comp, ContMDiffAt.coordChange, Bundle.Trivialization.mdifferentiableAt_snd_comp_iff₂, instFieldContMDiffRing, isInvertible_mfderivWithin_extChartAt_symm, mdifferentiable_prod_module_iff, VectorField.mlieBracketWithin_apply, MDifferentiable.neg, SmoothPartitionOfUnity.toPartitionOfUnity_toFun, Bundle.Trivialization.contMDiffOn_iff, SmoothPartitionOfUnity.contMDiff_smul, ContMDiff.prodMk_space, hasGroupoid_model_space, Bundle.Trivialization.mdifferentiableWithinAt_section_iff, LeftInvariantDerivation.ext_iff, mfderiv_subtype_coe_Icc_one, VectorField.mlieBracketWithin_eq_lieBracketWithin, MDifferentiableWithinAt.smul, VectorField.eventually_contMDiffWithinAt_mpullbackWithin_extChartAt_symm, DifferentiableAt.mdifferentiableAt, ContMDiffOn.smul, contMDiffOn_extend, Bundle.Trivialization.contMDiffWithinAt_snd_comp_iff₂, mdifferentiableAt_localFrame_coeff, StructureGroupoid.LocalInvariantProp.liftPropOn_chart_symm, contMDiffAt_pi_space, exists_smooth_zero_one_nhds_of_isClosed, contMDiffOn_iff_target, contMDiffOn_symm_of_mem_maximalAtlas, contMDiffOn_vectorSpace_iff_contDiffOn, mfderiv_neg, contMDiffAt_iff_target, LeftInvariantDerivation.toFun_eq_coe, UpperHalfPlane.contMDiff_denom, Manifold.exists_lt_of_riemannianEDist_lt, Bundle.Trivialization.contMDiffOn_section_iff, ContMDiffWithinAt.cle_arrowCongr, SmoothBumpCovering.embeddingPiTangent_coe, E2_mdifferentiable, EisensteinSeries.eisensteinSeriesSIF_mdifferentiable, SmoothPartitionOfUnity.nonneg', HasMFDerivWithinAt.prod, SmoothPartitionOfUnity.IsSubordinate.contMDiff_finsum_smul, HasMFDerivAt.mul', inTangentCoordinates_model_space, UpperHalfPlane.mdifferentiable_denom_zpow, MDifferentiableWithinAt.pow, StructureGroupoid.LocalInvariantProp.liftPropAt_chart, exists_contMDiffMap_one_nhds_of_subset_interior, StructureGroupoid.id_mem_maximalAtlas, SmoothPartitionOfUnity.sum_le_one, ModelWithCorners.mdifferentiableWithinAt_symm, MDifferentiableWithinAt.clm_prodMap, ContMDiffAt.clm_comp, contMDiffOn_prod_module_iff, eventually_norm_mfderiv_extChartAt_lt, Bundle.Trivialization.mdifferentiableWithinAt_snd_comp_iff₂, ContMDiffWithinAt.inner_bundle, mdifferentiableWithinAt_hom_bundle, Derivative.serreDerivative_mdifferentiable, MDifferentiableWithinAt.change_section_trivialization, MDifferentiable.prod, mdifferentiableOn_atlas_symm, UpperHalfPlane.mdifferentiable_iff, Bundle.Trivialization.contMDiffOn_symm_trans, exists_contMDiffMap_forall_mem_convex_of_local_const, smooth_functions_tower, mdifferentiable_iff_differentiable, mdifferentiableAt_atlas, Manifold.exists_lt_locally_constant_of_riemannianEDist_lt, ContinuousLinearEquiv.mdifferentiableAt, MDifferentiableWithinAt.clm_apply, UniqueDiffOn.uniqueMDiffOn, mdifferentiableAt_extChartAt, inCoordinates_tangent_bundle_core_model_space, ContMDiffAt.cle_arrowCongr, UpperHalfPlane.mdifferentiableAt_ofComplex, MDifferentiableOn.pow, Bundle.Trivialization.mdifferentiableAt_totalSpace_iff, hasMFDerivWithinAt_iff_hasFDerivWithinAt, LeftInvariantDerivation.instLinearMapClassContMDiffMapModelWithCornersSelfSomeENatTop, LeftInvariantDerivation.coeFnAddMonoidHom_apply, contMDiff_snd_tangentBundle_modelSpace, contMDiffWithinAt_hom_bundle, ContDiffWithinAt.comp_contMDiffWithinAt, mem_contMDiffFiberwiseLinear_iff, ContinuousLinearMap.contMDiffAt, contMDiffAt_iff_contDiffAt, Derivation.evalAt_apply, mdifferentiableWithinAt_iff_target, const_smul_mfderiv, HasMFDerivAt.const_smul, MDifferentiable.inner_bundle, ContinuousLinearMap.mdifferentiableAt, ContMDiff.cle_arrowCongr, DifferentiableAt.comp_mdifferentiableAt, ContDiff.comp_contMDiffAt, SmoothBumpCovering.toSmoothPartitionOfUnity_zero_of_zero, MDifferentiableWithinAt.prod, ContMDiff.coordChangeL, SmoothPartitionOfUnity.contMDiff_sum, Bundle.Trivialization.Bundle.Trivialization.mdifferentiable, contMDiffOn_projIcc, Metric.exists_contMDiffMap_forall_closedEBall_subset, contMDiff_circleExp, chartAt_self_eq, ContMDiffMap.coeFnLinearMap_apply, VectorField.mlieBracket_smul_right, MDifferentiable.pow, MDifferentiableWithinAt.sum, MDifferentiableAt.clm_apply, ContinuousLinearEquiv.mfderivWithin_eq, contMDiffOn_iff_localFrame_coeff, MDifferentiableWithinAt.neg, ModelWithCorners.mdifferentiableWithinAt, LeftInvariantDerivation.evalAt_apply
instTopologicalSpaceModelPi 📖	CompOp	1 math math: piChartedSpace_chartAt
instTopologicalSpaceModelProd 📖	CompOp	354 math math: TangentBundle.tangentMap_tangentBundle_pure, contMDiff_prod_assoc, mfderiv_prod_eq_add, Prod.instLieGroup, Bundle.ContMDiffRiemannianMetric.contMDiff, Bundle.mdifferentiableAt_proj, mdifferentiableAt_sub_section, ContMDiffMul.prod, MDifferentiableOn.finsum_section_of_locallyFinite, ModelWithCorners.range_prod, Bundle.contMDiffOn_zeroSection, MDifferentiableAt.clm_bundle_apply, MDifferentiableAt.mfderiv_prod, mdifferentiableWithinAt_totalSpace, contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt, ContMDiffOn.prodMk, tangentMapWithin_prodSnd, ContMDiffOn.mlieBracketWithin_vectorField, ContMDiffWithinAt.mlieBracketWithin_vectorField, mdifferentiableAt_iff_localFrame_coeff, Bundle.Trivialization.contMDiffOn_section_baseSet_iff, MDifferentiableOn.smul_const_section, tangentMap_chart, ContMDiffWithinAt.sub_section, Manifold.IsImmersionOfComplement.prodMap, contMDiff_addInvariantVectorField, mdifferentiableWithinAt_smul_const_section, TangentBundle.coe_chartAt_fst, mdifferentiableAt_add_section, HasMFDerivWithinAt.prodMk, ContMDiffAt.finsum_section_of_locallyFinite, ContMDiffAdd.prod, ContMDiffMul.contMDiff_mul, Bundle.contMDiffWithinAt_zeroSection, mdifferentiableOn_snd, contMDiff_mul, contMDiff_mulInvariantVectorField, contMDiffWithinAt_snd, Bundle.Trivialization.contMDiffOn, contMDiffWithinAt_prod_iff, UniqueMDiffOn.prod, MDifferentiableWithinAt.finsum_section_of_locallyFinite, IsLocalFrameOn.contMDiffAt_of_coeff, contMDiff_equivTangentBundleProd_symm, mdifferentiableWithinAt_section, contMDiffOn_baseSet_iff_localFrame_coeff, ContMDiffWithinAt.add_section, ContMDiffAt.add_section, ContMDiffAdd.contMDiff_add, Manifold.IsSmoothEmbedding.prodMap, MDifferentiable.clm_bundle_apply₂, Manifold.IsImmersionAtOfComplement.prodMap, Diffeomorph.coe_prodCongr, tangentBundle_model_space_coe_chartAt, hasMFDerivAt_fst, writtenInExtChart_prod, Bundle.contMDiffAt_zeroSection, ModelWithCorners.prod_target, contMDiffAt_mulInvariantVectorField, MDifferentiable.prodMap, equivTangentBundleProd_apply, MDifferentiable.clm_bundle_apply, MDifferentiableWithinAt.clm_bundle_apply₂, HasMFDerivWithinAt.prodMap, mdifferentiableAt_addInvariantVectorField, ContMDiff.sum_section_of_locallyFinite, ContMDiff.contMDiff_tangentMap, MDifferentiableAt.mpullback_vectorField, ContMDiffWithinAt.sum_section, MDifferentiableAt.sum_section, mdifferentiableAt_fst, Bundle.Trivialization.mdifferentiableAt_section_iff, MDifferentiableOn.prodMk, mfderiv_prod_eq_add_comp, MDifferentiableAt.prodMap', ContMDiffAt.prodMap, mdifferentiableAt_totalSpace, mdifferentiableOn_fst, mdifferentiable_mulInvariantVectorField, FiberBundle.chartedSpace_chartAt, ContMDiffOn.finsum_section_of_locallyFinite, MDifferentiableOn.sum_section_of_locallyFinite, MDifferentiableAt.prodMk, ContMDiffWithinAt.neg_section, Diffeomorph.prodCongr_symm, ContMDiffWithinAt.mpullbackWithin_vectorField_inter, mdifferentiableAt_hom_bundle, IsLocalFrameOn.mdifferentiableAt_of_coeff_aux, mdifferentiable_fst, mdifferentiableWithinAt_neg_section, modelWithCorners_prod_coe, Bundle.TotalSpace.isManifold, ContMDiffAt.const_smul_section, contMDiff_vectorSpace_iff_contDiff, mdifferentiableAt_snd, ContMDiffOn.mpullbackWithin_vectorField_inter, mfderiv_prodMap, ContMDiffAt.clm_apply_of_inCoordinates, Bundle.Trivialization.mdifferentiableWithinAt_totalSpace_iff, MDifferentiable.mpullback_vectorField, mdifferentiable_smul_const_section, Bundle.Trivialization.mdifferentiableOn_section_baseSet_iff, UniqueMDiffWithinAt.bundle_preimage', FiberBundle.exists_contMDiffOn_extend, MDifferentiableAt.finsum_section_of_locallyFinite, IsContMDiffRiemannianBundle.exists_contMDiff, ModelWithCorners.prod_symm_apply, contMDiff_snd, ContMDiffAt.clm_bundle_apply, contMDiffAt_prod_iff, tangentMap_prodSnd, mdifferentiableAt_neg_section, Bundle.Trivialization.contMDiffOn_localFrame_baseSet, HasMFDerivAt.prodMap, MDifferentiableAt.clm_bundle_apply₂, ContMDiffWithinAt.mpullback_vectorField_of_mem_nhdsWithin_of_eq, FiberBundle.writtenInExtChartAt_trivializationAt, IsLocalFrameOn.mdifferentiableOn_of_coeff, ModelWithCorners.prod_source, ContMDiffWithinAt.mpullback_vectorField_preimage, hasMFDerivWithinAt_fst, MDifferentiableWithinAt.mpullbackWithin_vectorField_inter_of_eq, MDifferentiableOn.prodMap, MDifferentiableAt.smul_section, ContMDiffWithinAt.mpullback_vectorField_preimage_of_eq, FiberBundle.mdifferentiableAt_extend, modelWithCorners_prod_coe_symm, contMDiff_smul, MDifferentiableWithinAt.clm_apply_of_inCoordinates, prodChartedSpace_chartAt, Bundle.mdifferentiableWithinAt_proj, IsLocalFrameOn.contMDiffOn, MDifferentiableOn.clm_bundle_apply, MDifferentiableWithinAt.prodMk, Bundle.Trivialization.mdifferentiableOn_section_iff, tangentMapWithin_prodFst, ContMDiffWithinAt.finsum_section_of_locallyFinite, Bundle.contMDiffWithinAt_totalSpace, Diffeomorph.coe_prodComm, Bundle.Trivialization.contMDiffWithinAt_iff, mdifferentiableWithinAt_sub_section, Bundle.mdifferentiableOn_proj, mdifferentiableWithinAt_add_section, ContMDiffWithinAt.mpullbackWithin_vectorField', tangentBundle_model_space_coe_chartAt_symm, tangentBundleModelSpaceHomeomorph_coe, equivTangentBundleProd_symm_apply_snd, MDifferentiable.sum_section, ContMDiffWithinAt.clm_bundle_apply₂, TangentBundle.chartAt, IsLocalFrameOn.contMDiffAt, contMDiffAt_hom_bundle, ContMDiffOn.prodMap, MDifferentiable.sum_section_of_locallyFinite, ContMDiffRing.contMDiff_mul, contMDiff_prod_iff, FiberBundle.extChartAt, MDifferentiableWithinAt.sum_section_of_locallyFinite, ContMDiffAt.mlieBracket_vectorField, ContMDiffOn.add_section, mfderiv_prod_right, writtenInExtChartAt_prod, ContMDiff.finsum_section_of_locallyFinite, Bundle.contMDiffWithinAt_proj, ModelWithCorners.boundary_of_boundaryless_left, Bundle.contMDiffAt_totalSpace, MDifferentiableAt.clm_apply_of_inCoordinates, ContMDiffWithinAt.clm_bundle_apply, ContMDiff.clm_bundle_apply, UniqueMDiffOn.tangentBundle_proj_preimage, tangentBundle_model_space_chartAt, TangentBundle.mem_chart_target_iff, ContMDiff.clm_bundle_apply₂, mdifferentiable_snd, MDifferentiableOn.sum_section, mdifferentiableAt_prod_iff, MDifferentiable.prodMk, FiberBundle.contMDiffAt_extend', contMDiffWithinAt_fst, Bundle.contMDiffOn_proj, ContMDiffWithinAt.prodMk, Bundle.contMDiff_proj, contMDiffOn_fst, MDifferentiableAt.sum_section_of_locallyFinite, MDifferentiableOn.mpullback_vectorField_preimage, contMDiffOn_prod_iff, ContMDiffWithinAt.mpullbackWithin_vectorField_of_mem_of_eq, Manifold.IsImmersionAt.prodMap, IsManifold.prod, mfderivWithin_prodMap, tangentMap_chart_symm, UniqueMDiffWithinAt.bundle_preimage, contMDiffAt_vectorSpace_iff_contDiffAt, ContMDiff.neg_section, Manifold.IsImmersion.prodMap, Bundle.mdifferentiableWithinAt_zeroSection, mfderiv_snd, mdifferentiable_addInvariantVectorField, VectorField.contMDiffWithinAt_mpullbackWithin_extChartAt_symm, modelWithCorners_prod_toPartialEquiv, Bundle.Trivialization.contMDiff_iff, ContMDiffWithinAt.sum_section_of_locallyFinite, Bundle.contMDiff_zeroSection, ContDiff.mlieBracket_vectorField, FiberBundle.extChartAt_target, contMDiffAt_localFrame_of_mem, mdifferentiableWithinAt_snd, mfderiv_prodMk, hasMFDerivWithinAt_snd, mdifferentiableAt_section, Bundle.Trivialization.contMDiffAt_section_iff, Bundle.mdifferentiable_proj, ContMDiffWithinAt.clm_apply_of_inCoordinates, FiberBundle.writtenInExtChartAt_trivializationAt_symm, ModelWithCorners.boundary_of_boundaryless_right, ContMDiffAt.sub_section, ModelWithCorners.range_eq_univ_prod, ModelWithCorners.prod_apply, tangentBundleModelSpaceHomeomorph_coe_symm, MDifferentiableWithinAt.mpullback_vectorField_preimage, MDifferentiableWithinAt.clm_bundle_apply, ContMDiffSection.contMDiff, IsManifold.mem_maximalAtlas_prod, contMDiff_equivTangentBundleProd, UniqueMDiffOn.bundle_preimage, Bundle.Trivialization.contMDiffAt_iff, ContMDiffOn.const_smul_section, Bundle.contMDiffAt_section, Bundle.Trivialization.contMDiffWithinAt_section, ModelWithCorners.boundary_prod, MDifferentiableOn.mpullbackWithin_vectorField_inter, ContMDiffAt.clm_bundle_apply₂, ContMDiffWithinAt.mpullbackWithin_vectorField_inter_of_eq, mDifferentiableOn_sub_section, equivTangentBundleProd_eq_tangentMap_prod_tangentMap, mdifferentiable_prod_iff, mdifferentiableOn_prod_iff, Bundle.Trivialization.contMDiffOn_symm, mdifferentiableAt_mulInvariantVectorField, mfderivWithin_prodMk, contMDiffAt_iff_localFrame_coeff, ContMDiffOn.sum_section_of_locallyFinite, ContMDiffAt.prodMap', tangentMap_prodFst, ContMDiffCovariantDerivativeOn.contMDiff, MDifferentiableWithinAt.mpullbackWithin_vectorField_inter, ContMDiffOn.contMDiffOn_tangentMapWithin, mdifferentiable_sub_section, ContMDiffWithinAt.const_smul_section, mdifferentiable_neg_section, ContMDiffWithinAt.prodMap', ContMDiffAt.sum_section_of_locallyFinite, mdifferentiableWithinAt_fst, MDifferentiable.finsum_section_of_locallyFinite, ContMDiffOn.mpullback_vectorField_preimage, IsLocalFrameOn.contMDiffOn_of_coeff, ModelWithCorners.BoundarylessManifold.prod, contMDiff_add, FiberBundle.exists_mdifferentiableOn_extend, Diffeomorph.prodComm_symm, Prod.instLieAddGroup, HasMFDerivAt.prodMk, ContMDiff.sub_section, MDifferentiableWithinAt.mpullback_vectorField_preimage_of_eq, ContMDiffWithinAt.mpullbackWithin_vectorField, ContMDiffAt.prodMk, Bundle.contMDiffAt_proj, contMDiffAt_addInvariantVectorField, contMDiff_tangentBundleModelSpaceHomeomorph, MDifferentiableAt.smul_const_section, ContMDiffAt.mpullback_vectorField_preimage, ContMDiffOn.smul_section_of_tsupport, ContMDiffWithinAt.smul_section, mdifferentiable_add_section, hasMFDerivAt_snd, hom_chart, MDifferentiableOn.smul_section, MDifferentiableWithinAt.prodMap, TangentBundle.coe_chartAt_symm_fst, Bundle.contMDiffWithinAt_section, Bundle.mdifferentiableOn_zeroSection, ContMDiffSection.mdifferentiable', contMDiff_tangentBundleModelSpaceHomeomorph_symm, mfderiv_fst, mfderivWithin_fst, ContMDiffWithinAt.mpullbackWithin_vectorField_of_eq, ContMDiffOn.sub_section, ContMDiffSection.mdifferentiableAt, MDifferentiableOn.smul_section_of_tsupport, ContMDiff.add_section, ContMDiffOn.sum_section, ContMDiffOn.neg_section, UniqueMDiffWithinAt.prod, equivTangentBundleProd_symm_apply_proj, ContMDiffSection.mdifferentiable, Bundle.Trivialization.contMDiffOn_iff, ContMDiffWithinAt.prodMap, mdifferentiable_smul_section, Bundle.mdifferentiable_zeroSection, Bundle.Trivialization.mdifferentiableWithinAt_section_iff, contMDiffAt_fst, mdifferentiableWithinAt_prod_iff, ContMDiffWithinAt.mpullbackWithin_vectorField_of_mem, VectorField.eventually_contMDiffWithinAt_mpullbackWithin_extChartAt_symm, IsLocalFrameOn.mdifferentiableAt_of_coeff, TangentBundle.chartAt_toPartialEquiv, ContMDiffAt.sum_section, ContMDiff.const_smul_section, tangentMap_prod_right, contMDiffOn_vectorSpace_iff_contDiffOn, ContMDiffOn.clm_bundle_apply, Bundle.Trivialization.contMDiffOn_section_iff, tangentMap_prod_left, mdifferentiableOn_add_section, FiberBundle.chartedSpace_chartAt_symm_fst, ContMDiffSection.contMDiff_toFun, ContMDiffAt.smul_section, contDiffGroupoid_prod, ModelWithCorners.interior_prod, contMDiffOn_snd, mfderiv_prod_left, ContMDiffAt.neg_section, MDifferentiableWithinAt.prodMap', mdifferentiableWithinAt_hom_bundle, IsLocalFrameOn.contMDiffAt_of_coeff_aux, Bundle.Trivialization.contMDiffOn_symm_trans, contMDiff_fst, Bundle.mdifferentiableAt_zeroSection, boundary_product, MDifferentiableAt.prodMap, ContMDiff.sum_section, mdifferentiableOn_neg_section, Bundle.Trivialization.mdifferentiableAt_totalSpace_iff, ContMDiff.prodMap, contMDiff_snd_tangentBundle_modelSpace, ContMDiffWithinAt.mpullbackWithin_vectorField_of_eq', contMDiffWithinAt_hom_bundle, mfderivWithin_snd, MDifferentiableOn.clm_bundle_apply₂, contMDiffAt_snd, ContMDiffOn.clm_bundle_apply₂, mfderiv_prod_eq_add_apply, extChartAt_prod, ContMDiff.mpullback_vectorField, Bundle.Trivialization.Bundle.Trivialization.mdifferentiable, TangentBundle.mem_chart_source_iff, MDifferentiableWithinAt.sum_section, ContMDiff.smul_section, ContMDiffWithinAt.mpullback_vectorField_of_mem_nhdsWithin, Manifold.LiftSourceTargetPropertyAt.prodMap, MDifferentiableWithinAt.smul_section, ContMDiffOn.smul_section, contMDiffOn_iff_localFrame_coeff, ContMDiff.prodMk
modelPiInhabited 📖	CompOp	—
modelProdInhabited 📖	CompOp	—
piChartedSpace 📖	CompOp	1 math math: piChartedSpace_chartAt
prodChartedSpace 📖	CompOp	120 math math: contMDiff_prod_assoc, mfderiv_prod_eq_add, Prod.instLieGroup, ContMDiffMul.prod, MDifferentiableAt.mfderiv_prod, ContMDiffOn.prodMk, tangentMapWithin_prodSnd, Manifold.IsImmersionOfComplement.prodMap, chartedSpaceSelf_prod, HasMFDerivWithinAt.prodMk, ContMDiffAdd.prod, ContMDiffMul.contMDiff_mul, mdifferentiableOn_snd, contMDiff_mul, contMDiffWithinAt_snd, Bundle.Trivialization.contMDiffOn, contMDiffWithinAt_prod_iff, UniqueMDiffOn.prod, contMDiff_equivTangentBundleProd_symm, ContMDiffAdd.contMDiff_add, Manifold.IsSmoothEmbedding.prodMap, Manifold.IsImmersionAtOfComplement.prodMap, Diffeomorph.coe_prodCongr, hasMFDerivAt_fst, writtenInExtChart_prod, MDifferentiable.prodMap, equivTangentBundleProd_apply, HasMFDerivWithinAt.prodMap, mdifferentiableAt_fst, MDifferentiableOn.prodMk, mfderiv_prod_eq_add_comp, MDifferentiableAt.prodMap', ContMDiffAt.prodMap, mdifferentiableOn_fst, MDifferentiableAt.prodMk, Diffeomorph.prodCongr_symm, mdifferentiable_fst, mdifferentiableAt_snd, mfderiv_prodMap, contMDiff_snd, contMDiffAt_prod_iff, tangentMap_prodSnd, HasMFDerivAt.prodMap, FiberBundle.writtenInExtChartAt_trivializationAt, hasMFDerivWithinAt_fst, MDifferentiableOn.prodMap, contMDiff_smul, prodChartedSpace_chartAt, MDifferentiableWithinAt.prodMk, tangentMapWithin_prodFst, Diffeomorph.coe_prodComm, equivTangentBundleProd_symm_apply_snd, ContMDiffOn.prodMap, ContMDiffRing.contMDiff_mul, contMDiff_prod_iff, mfderiv_prod_right, writtenInExtChartAt_prod, ModelWithCorners.boundary_of_boundaryless_left, mdifferentiable_snd, mdifferentiableAt_prod_iff, MDifferentiable.prodMk, contMDiffWithinAt_fst, ContMDiffWithinAt.prodMk, contMDiffOn_fst, contMDiffOn_prod_iff, Manifold.IsImmersionAt.prodMap, IsManifold.prod, mfderivWithin_prodMap, Manifold.IsImmersion.prodMap, mfderiv_snd, mdifferentiableWithinAt_snd, mfderiv_prodMk, hasMFDerivWithinAt_snd, FiberBundle.writtenInExtChartAt_trivializationAt_symm, ModelWithCorners.boundary_of_boundaryless_right, IsManifold.mem_maximalAtlas_prod, contMDiff_equivTangentBundleProd, ModelWithCorners.boundary_prod, equivTangentBundleProd_eq_tangentMap_prod_tangentMap, mdifferentiable_prod_iff, mdifferentiableOn_prod_iff, Bundle.Trivialization.contMDiffOn_symm, mfderivWithin_prodMk, ContMDiffAt.prodMap', tangentMap_prodFst, ContMDiffWithinAt.prodMap', mdifferentiableWithinAt_fst, ModelWithCorners.BoundarylessManifold.prod, contMDiff_add, Diffeomorph.prodComm_symm, Prod.instLieAddGroup, HasMFDerivAt.prodMk, ContMDiffAt.prodMk, hasMFDerivAt_snd, MDifferentiableWithinAt.prodMap, mfderiv_fst, mfderivWithin_fst, UniqueMDiffWithinAt.prod, equivTangentBundleProd_symm_apply_proj, ContMDiffWithinAt.prodMap, contMDiffAt_fst, mdifferentiableWithinAt_prod_iff, tangentMap_prod_right, tangentMap_prod_left, ModelWithCorners.interior_prod, contMDiffOn_snd, mfderiv_prod_left, MDifferentiableWithinAt.prodMap', Bundle.Trivialization.contMDiffOn_symm_trans, contMDiff_fst, boundary_product, MDifferentiableAt.prodMap, ContMDiff.prodMap, mfderivWithin_snd, contMDiffAt_snd, mfderiv_prod_eq_add_apply, extChartAt_prod, Bundle.Trivialization.Bundle.Trivialization.mdifferentiable, Manifold.LiftSourceTargetPropertyAt.prodMap, ContMDiff.prodMk

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
achart_def 📖	mathematical	—	achart OpenPartialHomeomorph Set Set.instMembership atlas chartAt chart_mem_atlas	—	—
achart_val 📖	mathematical	—	OpenPartialHomeomorph Set Set.instMembership atlas achart chartAt	—	—
chartAt_comp 📖	mathematical	—	chartAt ChartedSpace.comp OpenPartialHomeomorph.trans OpenPartialHomeomorph.toFun'	—	—
chartAt_self_eq 📖	mathematical	—	chartAt chartedSpaceSelf OpenPartialHomeomorph.refl	—	—
chart_mem_atlas 📖	mathematical	—	OpenPartialHomeomorph Set Set.instMembership atlas chartAt	—	ChartedSpace.chart_mem_atlas
chart_source_mem_nhds 📖	mathematical	—	Set Filter Filter.instMembership nhds PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv chartAt	—	IsOpen.mem_nhds OpenPartialHomeomorph.open_source mem_chart_source
chart_target_mem_nhds 📖	mathematical	—	Set Filter Filter.instMembership nhds OpenPartialHomeomorph.toFun' chartAt PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv	—	IsOpen.mem_nhds OpenPartialHomeomorph.open_target mem_chart_target
chartedSpaceSelf_atlas 📖	mathematical	—	OpenPartialHomeomorph Set Set.instMembership atlas chartedSpaceSelf OpenPartialHomeomorph.refl	—	—
chartedSpaceSelf_prod 📖	mathematical	—	prodChartedSpace chartedSpaceSelf instTopologicalSpaceProd	—	ChartedSpace.ext Set.image2_singleton_right Set.image_singleton OpenPartialHomeomorph.refl_prod_refl
chartedSpace_of_discreteTopology_chartAt 📖	mathematical	—	chartAt ChartedSpace.of_discreteTopology OpenPartialHomeomorph.const Unique.toInhabited isOpen_discrete Set Set.instSingletonSet Subsingleton.discreteTopology Unique.instSubsingleton	—	—
coe_achart 📖	mathematical	—	OpenPartialHomeomorph Set Set.instMembership atlas achart chartAt	—	—
iUnion_source_chartAt 📖	mathematical	—	Set.iUnion PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv chartAt Set.univ	—	Set.eq_univ_iff_forall Set.mem_iUnion mem_chart_source
isEmpty_of_chartedSpace 📖	mathematical	—	IsEmpty	—	isEmpty_or_nonempty IsEmpty.false
mem_achart_source 📖	mathematical	—	Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv OpenPartialHomeomorph atlas achart	—	mem_chart_source
mem_chart_source 📖	mathematical	—	Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv chartAt	—	ChartedSpace.mem_chart_source
mem_chart_target 📖	mathematical	—	Set Set.instMembership PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv chartAt OpenPartialHomeomorph.toFun'	—	OpenPartialHomeomorph.map_source mem_chart_source
modelProd_range_prod_id 📖	mathematical	—	Set.range ModelProd SProd.sprod Set Set.instSProd Set.univ	—	Set.prod_range_univ_eq
nonempty_of_chartedSpace 📖	—	—	—	—	—
piChartedSpace_chartAt 📖	mathematical	—	chartAt ModelPi instTopologicalSpaceModelPi Pi.topologicalSpace piChartedSpace OpenPartialHomeomorph.pi	—	—
prodChartedSpace_chartAt 📖	mathematical	—	chartAt ModelProd instTopologicalSpaceModelProd instTopologicalSpaceProd prodChartedSpace OpenPartialHomeomorph.prod	—	—
sum_chartAt_inl_apply 📖	mathematical	—	OpenPartialHomeomorph.toFun' instTopologicalSpaceSum chartAt ChartedSpace.sum	—	nonempty_of_chartedSpace Topology.IsOpenEmbedding.inl ChartedSpace.sum_chartAt_inl OpenPartialHomeomorph.lift_openEmbedding_apply
sum_chartAt_inr_apply 📖	mathematical	—	OpenPartialHomeomorph.toFun' instTopologicalSpaceSum chartAt ChartedSpace.sum	—	nonempty_of_chartedSpace Topology.IsOpenEmbedding.inr ChartedSpace.sum_chartAt_inr OpenPartialHomeomorph.lift_openEmbedding_apply

---

← Back to Index