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, partialHomeomorph, toChartedSpace, toTopologicalSpace, Manifold_type_tags, ModelPi, ModelProd, achart, atlas, chartAt, chartedSpaceSelf, instTopologicalSpaceModelPi, instTopologicalSpaceModelProd, modelPiInhabited, modelProdInhabited, piChartedSpace, prodChartedSpace	28
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	73

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	3 math math: StructureGroupoid.HasGroupoid.comp, chartAt_comp, extChartAt_comp
empty 📖	CompOp	—
of_discreteTopology 📖	CompOp	2 math math: chartedSpace_of_discreteTopology_chartAt, IsManifold.of_discreteTopology
sum 📖	CompOp	44 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, 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.lift_openEmbedding 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	—
partialHomeomorph 📖	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	222 math math: TangentBundle.tangentMap_tangentBundle_pure, contMDiff_prod_assoc, Prod.instLieGroup, Bundle.ContMDiffRiemannianMetric.contMDiff, Bundle.mdifferentiableAt_proj, Trivialization.mdifferentiableAt_section_iff, ContMDiffMul.prod, ModelWithCorners.range_prod, Bundle.contMDiffOn_zeroSection, MDifferentiableAt.mfderiv_prod, mdifferentiableWithinAt_totalSpace, contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt, ContMDiffOn.prodMk, tangentMap_chart, Manifold.IsImmersionOfComplement.prodMap, contMDiff_addInvariantVectorField, Trivialization.mdifferentiableOn_section_baseSet_iff, TangentBundle.coe_chartAt_fst, HasMFDerivWithinAt.prodMk, ContMDiffAdd.prod, ContMDiffMul.contMDiff_mul, Bundle.contMDiffWithinAt_zeroSection, mdifferentiableOn_snd, contMDiff_mul, contMDiff_mulInvariantVectorField, 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, tangentBundle_model_space_coe_chartAt, hasMFDerivAt_fst, writtenInExtChart_prod, Bundle.contMDiffAt_zeroSection, ModelWithCorners.prod_target, contMDiffAt_mulInvariantVectorField, MDifferentiable.prodMap, equivTangentBundleProd_apply, HasMFDerivWithinAt.prodMap, mdifferentiableAt_addInvariantVectorField, ContMDiff.contMDiff_tangentMap, mdifferentiableAt_fst, MDifferentiableOn.prodMk, MDifferentiableAt.prodMap', ContMDiffAt.prodMap, mdifferentiableAt_totalSpace, mdifferentiableOn_fst, mdifferentiable_mulInvariantVectorField, FiberBundle.chartedSpace_chartAt, 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, contMDiff_vectorSpace_iff_contDiff, mdifferentiableAt_snd, mfderiv_prodMap, UniqueMDiffWithinAt.bundle_preimage', IsContMDiffRiemannianBundle.exists_contMDiff, ModelWithCorners.prod_symm_apply, contMDiff_snd, contMDiffAt_prod_iff, tangentMap_prodSnd, HasMFDerivAt.prodMap, IsLocalFrameOn.mdifferentiableOn_of_coeff, ModelWithCorners.prod_source, hasMFDerivWithinAt_fst, MDifferentiableOn.prodMap, Trivialization.contMDiffOn_localFrame_baseSet, modelWithCorners_prod_coe_symm, contMDiff_smul, prodChartedSpace_chartAt, Bundle.mdifferentiableWithinAt_proj, IsLocalFrameOn.contMDiffOn, MDifferentiableWithinAt.prodMk, Bundle.contMDiffWithinAt_totalSpace, Diffeomorph.coe_prodComm, Bundle.mdifferentiableOn_proj, tangentBundle_model_space_coe_chartAt_symm, tangentBundleModelSpaceHomeomorph_coe, equivTangentBundleProd_symm_apply_snd, TangentBundle.chartAt, IsLocalFrameOn.contMDiffAt, contMDiffAt_hom_bundle, ContMDiffOn.prodMap, ContMDiffRing.contMDiff_mul, contMDiff_prod_iff, FiberBundle.extChartAt, mfderiv_prod_right, Bundle.contMDiffWithinAt_proj, ModelWithCorners.boundary_of_boundaryless_left, Bundle.contMDiffAt_totalSpace, Trivialization.contMDiffOn_section_baseSet_iff, UniqueMDiffOn.tangentBundle_proj_preimage, tangentBundle_model_space_chartAt, TangentBundle.mem_chart_target_iff, mdifferentiable_snd, mdifferentiableAt_prod_iff, MDifferentiable.prodMk, 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, tangentMap_chart_symm, UniqueMDiffWithinAt.bundle_preimage, contMDiffAt_vectorSpace_iff_contDiffAt, Manifold.IsImmersion.prodMap, Bundle.mdifferentiableWithinAt_zeroSection, mfderiv_snd, mdifferentiable_addInvariantVectorField, 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, ModelWithCorners.boundary_of_boundaryless_right, ModelWithCorners.range_eq_univ_prod, ModelWithCorners.prod_apply, tangentBundleModelSpaceHomeomorph_coe_symm, ContMDiffSection.contMDiff, IsManifold.mem_maximalAtlas_prod, contMDiff_equivTangentBundleProd, Trivialization.contMDiffWithinAt_iff, UniqueMDiffOn.bundle_preimage, Bundle.contMDiffAt_section, ModelWithCorners.boundary_prod, equivTangentBundleProd_eq_tangentMap_prod_tangentMap, mdifferentiable_prod_iff, mdifferentiableOn_prod_iff, mdifferentiableAt_mulInvariantVectorField, mfderivWithin_prodMk, modelProd_range_prod_id, Trivialization.mdifferentiableOn_section_iff, ContMDiffAt.prodMap', tangentMap_prodFst, ContMDiffOn.contMDiffOn_tangentMapWithin, ContMDiffWithinAt.prodMap', mdifferentiableWithinAt_fst, Trivialization.contMDiffAt_section_iff, IsLocalFrameOn.contMDiffOn_of_coeff, ModelWithCorners.BoundarylessManifold.prod, contMDiff_add, Diffeomorph.prodComm_symm, Prod.instLieAddGroup, HasMFDerivAt.prodMk, Trivialization.contMDiffOn_symm, ContMDiffAt.prodMk, Bundle.contMDiffAt_proj, Trivialization.contMDiffOn_iff, contMDiffAt_addInvariantVectorField, contMDiff_tangentBundleModelSpaceHomeomorph, hasMFDerivAt_snd, hom_chart, MDifferentiableWithinAt.prodMap, TangentBundle.coe_chartAt_symm_fst, 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, TangentBundle.chartAt_toPartialEquiv, tangentMap_prod_right, contMDiffOn_vectorSpace_iff_contDiffOn, tangentMap_prod_left, ContMDiffSection.contMDiff_toFun, contDiffGroupoid_prod, ModelWithCorners.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, contMDiff_snd_tangentBundle_modelSpace, contMDiffWithinAt_hom_bundle, contMDiffAt_snd, Trivialization.contMDiffWithinAt_section, extChartAt_prod, TangentBundle.mem_chart_source_iff, Manifold.LiftSourceTargetPropertyAt.prodMap, contMDiffOn_section_of_mem_baseSet, 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	23 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
chartAt 📖	CompOp	89 math math: ChartedSpace.sum_chartAt_inr, SmoothPartitionOfUnity.exists_isSubordinate_chartAt_source, writtenInExtChartAt_chartAt, TopologicalSpace.Opens.chartAt_eq, contMDiffOn_chart, chart_target_mem_nhds, TopologicalSpace.Opens.chartAt_subtype_val_symm_eventuallyEq, StructureGroupoid.LocalInvariantProp.liftPropAt_chart_symm, mem_chart_source, mdifferentiableOn_extChartAt, TangentBundle.coe_chartAt_fst, ChartedSpace.LiftPropWithinAt.prop, 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, FiberBundle.chartedSpace_chartAt, StructureGroupoid.chart_mem_maximalAtlas, SmoothBumpFunction.support_eq_inter_preimage, 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, 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, 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	428 math math: TangentBundle.continuousLinearMapAt_model_space, ContMDiffAt.coordChangeL, MDifferentiable.coordChangeL, UpperHalfPlane.mdifferentiable_num, SmoothBumpCovering.toSmoothPartitionOfUnity_eq_mul_prod, Trivialization.mdifferentiableAt_section_iff, LeftInvariantDerivation.lift_zero, exists_contMDiffMap_zero_one_of_isClosed, contMDiffAt_extend, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart', CuspFormClass.holo, LeftInvariantDerivation.leibniz, contMDiffWithinAt_iff_target, writtenInExtChartAt_chartAt, ContMDiffMap.coeFnAlgHom_apply, Manifold.pathELength_eq_lintegral_mfderiv_Ioo, ContDiffWithinAt.contMDiffWithinAt, mdifferentiableWithinAt_totalSpace, contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt, smoothSheafCommRing.nonunits_stalk, MDifferentiableWithinAt.differentiableWithinAt_mpullbackWithin_vectorField, contMDiffOn_chart, ContDiffAt.contMDiffAt, mdifferentiable_iff_target, contMDiffAt_iff_source, 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, SmoothPartitionOfUnity.nonneg, LeftInvariantDerivation.left_invariant', chartedSpaceSelf_prod, Trivialization.mdifferentiableOn_section_baseSet_iff, mdifferentiableOn_extChartAt, mdifferentiableOn_symm_coordChangeL, SmoothBumpCovering.exists_immersion_euclidean, IsOpen.exists_msmooth_support_eq, SmoothPartitionOfUnity.locallyFinite', ModelWithCorners.mdifferentiableOn_symm, ContinuousLinearEquiv.coe_toDiffeomorph_symm, hasMFDerivAt_extChartAt, ContinuousLinearMap.contMDiff, ContinuousLinearMap.mdifferentiable, instContMDiffAddSelf, mdifferentiable_chart, smoothSheafCommRing.instLocalRing_stalk, mdifferentiableWithinAt_section, Trivialization.contMDiffAt_iff, VectorBundleCore.contMDiffOn_coordChange, contMDiffOn_chart_symm, Trivialization.contMDiffOn_symm_trans, inTangentCoordinates_eq_mfderiv_comp, mfderivWithin_projIcc_one, Trivialization.contMDiff_iff, LeftInvariantDerivation.lift_add, contMDiffOn_isOpenEmbedding_symm, Trivialization.contMDiffOn_section_iff, StructureGroupoid.mem_maximalAtlas_of_mem_groupoid, tangentBundle_model_space_coe_chartAt, StructureGroupoid.LocalInvariantProp.liftPropAt_of_mem_groupoid, Trivialization.mdifferentiableWithinAt_snd_comp_iff₂, contMDiffOn_iff_contDiffOn, mfderivWithin_comp_projIcc_one, UpperHalfPlane.mdifferentiable_inv_denom, LeftInvariantDerivation.lift_smul, SmoothPartitionOfUnity.sum_finsupport', 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, extChartAt_self_apply, Manifold.pathELength_eq_lintegral_mfderivWithin_Icc, hasMFDerivAt_neg, ContinuousLinearEquiv.hasMFDerivAt, SmoothBumpCovering.toSmoothPartitionOfUnity_apply, SmoothPartitionOfUnity.contDiffAt_finsum, mdifferentiableOn_iff_target, contMDiff_isOpenEmbedding, 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, mfderiv_chartAt_eq_tangentCoordChange, DifferentiableWithinAt.mdifferentiableWithinAt, 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, UniqueDiffWithinAt.uniqueMDiffWithinAt, ContMDiffAt.mfderiv_const, smoothSheafCommRing.isUnit_stalk_iff, contMDiff_vectorSpace_iff_contDiff, LeftInvariantDerivation.map_zero, TangentBundle.coordChange_model_space, fdifferential_apply, SmoothBumpFunction.contMDiffAt, MDifferentiableOn.coordChangeL, mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm, ContMDiffMap.smul_comp, SmoothBumpCovering.sum_toSmoothPartitionOfUnity_eq, contMDiffAt_coordChangeL, contMDiff_subtype_coe_Icc, LeftInvariantDerivation.coe_sub, MDifferentiableWithinAt.coordChangeL, extChartAt_self_eq, FiberBundle.writtenInExtChartAt_trivializationAt, 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, SmoothPartitionOfUnity.mem_finsupport, IsOpen.exists_contMDiff_support_eq, DifferentiableOn.mdifferentiableOn, ContinuousLinearEquiv.mdifferentiableOn, mdifferentiableWithinAt_iff_differentiableWithinAt, contMDiff_smul, trivializationAt_model_space_apply, contMDiffOn_continuousLinearMapCoordChange, mfderiv_coe_sphere_injective, contMDiffOn_extChartAt_symm, chartedSpaceSelf_atlas, 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, SmoothBumpCovering.embeddingPiTangent_injective_mfderiv, ModelWithCorners.mdifferentiableAt, StructureGroupoid.liftPropWithinAt_self_target, 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, exists_msmooth_zero_iff_one_iff_of_isClosed, LeftInvariantDerivation.map_add, SmoothPartitionOfUnity.finsum_smul_mem_convex, LeftInvariantDerivation.coe_add, StructureGroupoid.LocalInvariantProp.liftPropOn_of_mem_groupoid, ContDiff.contMDiff, SmoothPartitionOfUnity.sum_le_one', instIsRiemannianManifoldModelWithCornersSelfReal, SmoothBumpCovering.embeddingPiTangent_ker_mfderiv, ContMDiffOn.inner_bundle, ModelWithCorners.hasMFDerivWithinAt, SmoothPartitionOfUnity.sum_nonneg, StructureGroupoid.LocalInvariantProp.liftPropOn_of_mem_maximalAtlas, Bundle.contMDiffAt_totalSpace, Diffeomorph.uniqueDiffOn_image, LeftInvariantDerivation.coe_injective, MDifferentiableWithinAt.inner_bundle, 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, tangentBundle_model_space_chartAt, mdifferentiableAt_iff_target_of_mem_source, ContMDiffWithinAt.mfderivWithin, IsOpen.exists_msmooth_support_eq_aux, ext_chart_model_space_apply, StructureGroupoid.liftPropWithinAt_self, exists_contMDiff_zero_iff_one_iff_of_isClosed, writtenInExtChartAt_extChartAt, StructureGroupoid.LocalInvariantProp.liftPropAt_symm_of_mem_maximalAtlas, 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, LeftInvariantDerivation.map_smul, oneTangentSpaceIcc_def, contMDiffAt_section_of_mem_baseSet, ModelWithCorners.uniqueMDiffOn, ModelWithCorners.hasMFDerivWithinAt_symm, SmoothPartitionOfUnity.sum_eq_one, mdifferentiableAt_neg, mdifferentiableOn_atlas, instContMDiffInv₀ModelWithCornersSelf, contMDiffOn_iff_source_of_mem_maximalAtlas, SmoothBumpCovering.embeddingPiTangent_injOn, contMDiffWithinAt_extChartAt_symm_target_self, StructureGroupoid.LocalInvariantProp.liftPropOn_chart, contMDiffAt_vectorSpace_iff_contDiffAt, contMDiffWithinAt_iff_contDiffWithinAt, PointedContMDiffMap.instIsScalarTowerSomeENatTopContMDiffMapModelWithCornersSelf, 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, 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', SmoothPartitionOfUnity.exists_pos_of_mem, FiberBundle.writtenInExtChartAt_trivializationAt_symm, 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, 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, Trivialization.contMDiffWithinAt_iff, 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, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_target, norm_tangentSpace_vectorSpace, mdifferentiableAt_iff_source_of_mem_source, contMDiffAt_prod_module_iff, mdifferentiable_of_mem_atlas, Trivialization.mdifferentiableOn_section_iff, mdifferentiable_jacobiTheta, SmoothBumpCovering.support_toSmoothPartitionOfUnity_subset, 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, Trivialization.contMDiffAt_section_iff, ContMDiffMap.smul_comp', ContMDiffAt.mfderiv, LeftInvariantDerivation.coe_zero, Trivialization.mdifferentiableAt_snd_comp_iff₂, UpperHalfPlane.contMDiffAt_iff, contMDiffOn_extend_symm, exists_embedding_euclidean_of_compact, VectorPrebundle.contMDiffOn_contMDiffCoordChange, LeftInvariantDerivation.toDerivation_injective, ContinuousLinearMap.contMDiffWithinAt, mdifferentiableAt_coordChangeL, writtenInExtChartAt_chartAt_symm, contMDiffAt_of_mem_maximalAtlas, mdifferentiableWithinAt_iff_source_of_mem_source, UpperHalfPlane.mdifferentiable_coe, Trivialization.contMDiffOn_symm, StructureGroupoid.LocalInvariantProp.liftPropOn_symm_of_mem_maximalAtlas, Trivialization.contMDiffOn_iff, Units.contMDiff_val, contMDiff_tangentBundleModelSpaceHomeomorph, 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, Trivialization.mdifferentiableWithinAt_totalSpace_iff, contMDiff_tangentBundleModelSpaceHomeomorph_symm, ContinuousLinearMap.contMDiffOn, StructureGroupoid.liftPropWithinAt_self_source, contMDiffOn_coordChangeL, contMDiffOn_model_symm, nnnorm_tangentSpace_vectorSpace, mfderiv_eq_fderiv, MDifferentiableAt.inner_bundle, EisensteinSeries.eisensteinSeries_SIF_MDifferentiable, ContinuousLinearMap.mdifferentiableOn, StructureGroupoid.LocalInvariantProp.liftPropAt_of_mem_maximalAtlas, LeftInvariantDerivation.commutator_apply, UpperHalfPlane.mdifferentiableAt_iff, LeftInvariantDerivation.commutator_coe_derivation, instFieldContMDiffRing, isInvertible_mfderivWithin_extChartAt_symm, mdifferentiable_prod_module_iff, VectorField.mlieBracketWithin_apply, SmoothPartitionOfUnity.toPartitionOfUnity_toFun, hasGroupoid_model_space, LeftInvariantDerivation.ext_iff, mfderiv_subtype_coe_Icc_one, VectorField.mlieBracketWithin_eq_lieBracketWithin, VectorField.eventually_contMDiffWithinAt_mpullbackWithin_extChartAt_symm, DifferentiableAt.mdifferentiableAt, 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, SmoothBumpCovering.embeddingPiTangent_coe, EisensteinSeries.eisensteinSeriesSIF_mdifferentiable, SmoothPartitionOfUnity.nonneg', inTangentCoordinates_model_space, UpperHalfPlane.mdifferentiable_denom_zpow, StructureGroupoid.LocalInvariantProp.liftPropAt_chart, exists_contMDiffMap_one_nhds_of_subset_interior, StructureGroupoid.id_mem_maximalAtlas, SmoothPartitionOfUnity.sum_le_one, ModelWithCorners.mdifferentiableWithinAt_symm, contMDiffOn_prod_module_iff, eventually_norm_mfderiv_extChartAt_lt, ContMDiffWithinAt.inner_bundle, mdifferentiableWithinAt_hom_bundle, Trivialization.contMDiffOn, mdifferentiableOn_atlas_symm, UpperHalfPlane.mdifferentiable_iff, contMDiffOn_section_of_mem_baseSet₀, 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, UniqueDiffOn.uniqueMDiffOn, mdifferentiableAt_extChartAt, inCoordinates_tangent_bundle_core_model_space, 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, MDifferentiable.inner_bundle, 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, chartAt_self_eq, ContMDiffMap.coeFnLinearMap_apply, contMDiffOn_section_of_mem_baseSet, ModelWithCorners.mdifferentiableWithinAt, LeftInvariantDerivation.evalAt_apply
instTopologicalSpaceModelPi 📖	CompOp	1 math math: piChartedSpace_chartAt
instTopologicalSpaceModelProd 📖	CompOp	221 math math: TangentBundle.tangentMap_tangentBundle_pure, contMDiff_prod_assoc, Prod.instLieGroup, Bundle.ContMDiffRiemannianMetric.contMDiff, Bundle.mdifferentiableAt_proj, Trivialization.mdifferentiableAt_section_iff, ContMDiffMul.prod, ModelWithCorners.range_prod, Bundle.contMDiffOn_zeroSection, MDifferentiableAt.mfderiv_prod, mdifferentiableWithinAt_totalSpace, contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt, ContMDiffOn.prodMk, tangentMap_chart, Manifold.IsImmersionOfComplement.prodMap, contMDiff_addInvariantVectorField, Trivialization.mdifferentiableOn_section_baseSet_iff, TangentBundle.coe_chartAt_fst, HasMFDerivWithinAt.prodMk, ContMDiffAdd.prod, ContMDiffMul.contMDiff_mul, Bundle.contMDiffWithinAt_zeroSection, mdifferentiableOn_snd, contMDiff_mul, contMDiff_mulInvariantVectorField, 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, tangentBundle_model_space_coe_chartAt, hasMFDerivAt_fst, writtenInExtChart_prod, Bundle.contMDiffAt_zeroSection, ModelWithCorners.prod_target, contMDiffAt_mulInvariantVectorField, MDifferentiable.prodMap, equivTangentBundleProd_apply, HasMFDerivWithinAt.prodMap, mdifferentiableAt_addInvariantVectorField, ContMDiff.contMDiff_tangentMap, mdifferentiableAt_fst, MDifferentiableOn.prodMk, MDifferentiableAt.prodMap', ContMDiffAt.prodMap, mdifferentiableAt_totalSpace, mdifferentiableOn_fst, mdifferentiable_mulInvariantVectorField, FiberBundle.chartedSpace_chartAt, 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, contMDiff_vectorSpace_iff_contDiff, mdifferentiableAt_snd, mfderiv_prodMap, UniqueMDiffWithinAt.bundle_preimage', IsContMDiffRiemannianBundle.exists_contMDiff, ModelWithCorners.prod_symm_apply, contMDiff_snd, contMDiffAt_prod_iff, tangentMap_prodSnd, HasMFDerivAt.prodMap, IsLocalFrameOn.mdifferentiableOn_of_coeff, ModelWithCorners.prod_source, hasMFDerivWithinAt_fst, MDifferentiableOn.prodMap, Trivialization.contMDiffOn_localFrame_baseSet, modelWithCorners_prod_coe_symm, contMDiff_smul, prodChartedSpace_chartAt, Bundle.mdifferentiableWithinAt_proj, IsLocalFrameOn.contMDiffOn, MDifferentiableWithinAt.prodMk, Bundle.contMDiffWithinAt_totalSpace, Diffeomorph.coe_prodComm, Bundle.mdifferentiableOn_proj, tangentBundle_model_space_coe_chartAt_symm, tangentBundleModelSpaceHomeomorph_coe, equivTangentBundleProd_symm_apply_snd, TangentBundle.chartAt, IsLocalFrameOn.contMDiffAt, contMDiffAt_hom_bundle, ContMDiffOn.prodMap, ContMDiffRing.contMDiff_mul, contMDiff_prod_iff, FiberBundle.extChartAt, mfderiv_prod_right, Bundle.contMDiffWithinAt_proj, ModelWithCorners.boundary_of_boundaryless_left, Bundle.contMDiffAt_totalSpace, Trivialization.contMDiffOn_section_baseSet_iff, UniqueMDiffOn.tangentBundle_proj_preimage, tangentBundle_model_space_chartAt, TangentBundle.mem_chart_target_iff, mdifferentiable_snd, mdifferentiableAt_prod_iff, MDifferentiable.prodMk, 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, tangentMap_chart_symm, UniqueMDiffWithinAt.bundle_preimage, contMDiffAt_vectorSpace_iff_contDiffAt, Manifold.IsImmersion.prodMap, Bundle.mdifferentiableWithinAt_zeroSection, mfderiv_snd, mdifferentiable_addInvariantVectorField, 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, ModelWithCorners.boundary_of_boundaryless_right, ModelWithCorners.range_eq_univ_prod, ModelWithCorners.prod_apply, tangentBundleModelSpaceHomeomorph_coe_symm, ContMDiffSection.contMDiff, IsManifold.mem_maximalAtlas_prod, contMDiff_equivTangentBundleProd, Trivialization.contMDiffWithinAt_iff, UniqueMDiffOn.bundle_preimage, Bundle.contMDiffAt_section, ModelWithCorners.boundary_prod, equivTangentBundleProd_eq_tangentMap_prod_tangentMap, mdifferentiable_prod_iff, mdifferentiableOn_prod_iff, mdifferentiableAt_mulInvariantVectorField, mfderivWithin_prodMk, Trivialization.mdifferentiableOn_section_iff, ContMDiffAt.prodMap', tangentMap_prodFst, ContMDiffOn.contMDiffOn_tangentMapWithin, ContMDiffWithinAt.prodMap', mdifferentiableWithinAt_fst, Trivialization.contMDiffAt_section_iff, IsLocalFrameOn.contMDiffOn_of_coeff, ModelWithCorners.BoundarylessManifold.prod, contMDiff_add, Diffeomorph.prodComm_symm, Prod.instLieAddGroup, HasMFDerivAt.prodMk, Trivialization.contMDiffOn_symm, ContMDiffAt.prodMk, Bundle.contMDiffAt_proj, Trivialization.contMDiffOn_iff, contMDiffAt_addInvariantVectorField, contMDiff_tangentBundleModelSpaceHomeomorph, hasMFDerivAt_snd, hom_chart, MDifferentiableWithinAt.prodMap, TangentBundle.coe_chartAt_symm_fst, 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, TangentBundle.chartAt_toPartialEquiv, tangentMap_prod_right, contMDiffOn_vectorSpace_iff_contDiffOn, tangentMap_prod_left, ContMDiffSection.contMDiff_toFun, contDiffGroupoid_prod, ModelWithCorners.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, contMDiff_snd_tangentBundle_modelSpace, contMDiffWithinAt_hom_bundle, contMDiffAt_snd, Trivialization.contMDiffWithinAt_section, extChartAt_prod, TangentBundle.mem_chart_source_iff, Manifold.LiftSourceTargetPropertyAt.prodMap, contMDiffOn_section_of_mem_baseSet, ContMDiff.prodMk
modelPiInhabited 📖	CompOp	—
modelProdInhabited 📖	CompOp	—
piChartedSpace 📖	CompOp	1 math math: piChartedSpace_chartAt
prodChartedSpace 📖	CompOp	112 math math: contMDiff_prod_assoc, Prod.instLieGroup, ContMDiffMul.prod, MDifferentiableAt.mfderiv_prod, ContMDiffOn.prodMk, Manifold.IsImmersionOfComplement.prodMap, chartedSpaceSelf_prod, HasMFDerivWithinAt.prodMk, ContMDiffAdd.prod, ContMDiffMul.contMDiff_mul, mdifferentiableOn_snd, contMDiff_mul, contMDiffWithinAt_snd, contMDiffWithinAt_prod_iff, UniqueMDiffOn.prod, contMDiff_equivTangentBundleProd_symm, Trivialization.contMDiffOn_symm_trans, 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, 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, Diffeomorph.coe_prodComm, equivTangentBundleProd_symm_apply_snd, ContMDiffOn.prodMap, ContMDiffRing.contMDiff_mul, contMDiff_prod_iff, mfderiv_prod_right, 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, mfderivWithin_prodMk, ContMDiffAt.prodMap', tangentMap_prodFst, ContMDiffWithinAt.prodMap', mdifferentiableWithinAt_fst, ModelWithCorners.BoundarylessManifold.prod, contMDiff_add, Diffeomorph.prodComm_symm, Prod.instLieAddGroup, HasMFDerivAt.prodMk, Trivialization.contMDiffOn_symm, ContMDiffAt.prodMk, hasMFDerivAt_snd, MDifferentiableWithinAt.prodMap, mfderiv_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', Trivialization.contMDiffOn, contMDiff_fst, boundary_product, MDifferentiableAt.prodMap, Trivialization.mdifferentiable, ContMDiff.prodMap, contMDiffAt_snd, extChartAt_prod, 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