| Metric | Count |
|---|
DefinitionstoPartialEquiv, toPartialEquivOfImageEq, transPartialEquiv, EqOnSource, restr, symm_apply, copy, disjointUnion, eqOnSourceSetoid, inhabitedOfEmpty, instCoeFunForall, instInhabited, invFun, ofSet, pi, piecewise, prod, refl, restr, single, source, target, toEquiv, toFun, trans, trans', transEquiv, toPartialEquiv, toPartialEquiv, mfldSetTac, mfld_cfg | 31 |
Theoremsrefl_toPartialEquiv, symm_toPartialEquiv, toPartialEquivOfImageEq_apply, toPartialEquivOfImageEq_source, toPartialEquivOfImageEq_symm_apply, toPartialEquivOfImageEq_target, toPartialEquiv_apply, toPartialEquiv_source, toPartialEquiv_symm_apply, toPartialEquiv_target, transPartialEquiv_apply, transPartialEquiv_eq_trans, transPartialEquiv_source, transPartialEquiv_symm_apply, transPartialEquiv_target, transPartialEquiv_trans, trans_toPartialEquiv, trans_transPartialEquiv, eqOn, restr, source_eq, source_inter_preimage_eq, symm', symm_eqOn, target_eq, trans', apply_mem_iff, compl, diff, iff_preimage_eq, iff_symm_preimage_eq, image_eq, inter, inter_eq_of_inter_eq_of_eqOn, leftInvOn_piecewise, mapsTo, of_image_eq, of_preimage_eq, of_symm_image_eq, of_symm_preimage_eq, preimage_eq, restr_apply, restr_source, restr_symm_apply, restr_target, symm_apply_mem_iff, symm_eq_on_of_inter_eq_of_eqOn, symm_iff, symm_image_eq, symm_mapsTo, symm_preimage_eq, union, bijOn, coe_mk, coe_symm_mk, coe_trans, coe_trans_symm, copy_apply, copy_eq, copy_source, copy_symm_apply, copy_target, disjointUnion_apply, disjointUnion_eq_piecewise, disjointUnion_source, disjointUnion_symm_apply, disjointUnion_target, eqOnSource_refl, eq_of_eqOnSource_univ, eq_symm_apply, exists_mem_target, ext, ext_iff, forall_mem_target, image_eq_target_inter_inv_preimage, image_source_eq_target, image_source_inter_eq, image_source_inter_eq', image_symm_image_of_subset_target, image_trans_source, injOn, injective_of_source_eq_univ, injective_symm_of_target_eq_univ, invFun_as_coe, invOn, inv_image_trans_target, isImage_source_target, isImage_source_target_of_disjoint, leftInvOn, left_inv, left_inv', map_source, map_source', map_source'', map_target, map_target', mapsTo, mem_symm_trans_source, ofSet_coe, ofSet_source, ofSet_symm, ofSet_target, pi_apply, pi_refl, pi_source, pi_symm, pi_symm_apply, pi_target, pi_trans, piecewise_apply, piecewise_source, piecewise_symm_apply, piecewise_target, prod_coe, prod_coe_symm, prod_source, prod_symm, prod_target, prod_trans, refl_coe, refl_prod_refl, refl_restr_source, refl_restr_target, refl_source, refl_symm, refl_target, refl_trans, restr_coe, restr_coe_symm, restr_eq_of_source_subset, restr_source, restr_target, restr_trans, restr_univ, rightInvOn, right_inv, right_inv', self_trans_symm, single_apply, single_source, single_symm_apply, single_target, source_inter_preimage_inv_preimage, source_inter_preimage_target_inter, source_restr_subset_source, source_subset_preimage_target, surjOn, surjective_of_target_eq_univ, surjective_symm_of_source_eq_univ, symm_bijective, symm_image_eq_source_inter_preimage, symm_image_image_of_subset_source, symm_image_target_eq_source, symm_image_target_inter_eq, symm_image_target_inter_eq', symm_mapsTo, symm_piecewise, symm_source, symm_symm, symm_target, symm_trans_self, target_inter_inv_preimage_preimage, target_subset_preimage_source, target_subset_range, trans'_apply, trans'_source, trans'_symm_apply, trans'_target, transEquiv_apply, transEquiv_eq_trans, transEquiv_source, transEquiv_symm_apply, transEquiv_target, transEquiv_transEquiv, trans_apply, trans_assoc, trans_ofSet, trans_refl, trans_refl_restr, trans_refl_restr', trans_source, trans_source', trans_source'', trans_symm_eq_symm_trans_symm, trans_target, trans_target', trans_target'', trans_transEquiv, toPartialEquiv_apply, toPartialEquiv_source, toPartialEquiv_symm_apply, toPartialEquiv_target | 192 |
| Total | 223 |
| Name | Category | Theorems |
|---|
EqOnSource 📖 | MathDef | 1 mathmath: OpenPartialHomeomorph.eqOnSource_iff
|
copy 📖 | CompOp | 5 mathmath: copy_target, copy_apply, copy_symm_apply, copy_eq, copy_source
|
disjointUnion 📖 | CompOp | 5 mathmath: disjointUnion_apply, disjointUnion_eq_piecewise, disjointUnion_source, disjointUnion_symm_apply, disjointUnion_target
|
eqOnSourceSetoid 📖 | CompOp | 4 mathmath: symm_trans_self, eqOnSource_refl, self_trans_symm, FiberBundleCore.localTrivAsPartialEquiv_trans
|
inhabitedOfEmpty 📖 | CompOp | — |
instCoeFunForall 📖 | CompOp | — |
instInhabited 📖 | CompOp | — |
invFun 📖 | CompOp | 12 mathmath: ModelWithCorners.continuous_invFun, right_inv', Equidecomp.restr_invFun, ModelWithCorners.ext_iff, invFun_as_coe, OpenPartialHomeomorph.continuousOn_invFun, Pretrivialization.domExtend_invFun, Continuous.invFun, OpenPartialHomeomorph.invFun_eq_coe, left_inv', PartialDiffeomorph.contMDiffOn_invFun, map_target'
|
ofSet 📖 | CompOp | 8 mathmath: OpenPartialHomeomorph.ofSet_toPartialEquiv, symm_trans_self, ofSet_symm, ofSet_target, ofSet_source, ofSet_coe, trans_ofSet, self_trans_symm
|
pi 📖 | CompOp | 8 mathmath: pi_trans, pi_target, OpenPartialHomeomorph.pi_toPartialEquiv, pi_source, pi_apply, pi_refl, pi_symm, pi_symm_apply
|
piecewise 📖 | CompOp | 7 mathmath: piecewise_source, disjointUnion_eq_piecewise, symm_piecewise, piecewise_apply, piecewise_target, piecewise_symm_apply, OpenPartialHomeomorph.piecewise_toPartialEquiv
|
prod 📖 | CompOp | 14 mathmath: ModelWithCorners.prod_target, prod_source, prod_coe_symm, prod_trans, OpenPartialHomeomorph.prod_toPartialEquiv, FiberBundle.extChartAt, OpenPartialHomeomorph.extend_prod, prod_coe, modelWithCorners_prod_toPartialEquiv, prod_symm, TangentBundle.chartAt_toPartialEquiv, refl_prod_refl, prod_target, extChartAt_prod
|
refl 📖 | CompOp | 19 mathmath: OpenPartialHomeomorph.refl_partialEquiv, refl_restr_target, refl_restr_source, trans_refl_restr, trans_refl_restr', Equidecomp.refl_toPartialEquiv, FiberBundle.extChartAt, refl_symm, extChartAt_model_space_eq_id, refl_source, trans_refl, Equiv.refl_toPartialEquiv, modelWithCornersSelf_partialEquiv, refl_target, refl_coe, TangentBundle.chartAt_toPartialEquiv, refl_trans, refl_prod_refl, pi_refl
|
restr 📖 | CompOp | 18 mathmath: restr_target, restr_eq_of_source_subset, EqOnSource.restr, restr_univ, OpenPartialHomeomorph.restr_toPartialEquiv, refl_restr_target, refl_restr_source, trans_refl_restr, trans_refl_restr', restr_coe_symm, source_restr_subset_source, restr_coe, OpenPartialHomeomorph.restr_toPartialEquiv', Equidecomp.toPartialEquiv_restr, OpenPartialHomeomorph.restrOpen_toPartialEquiv, trans_ofSet, restr_trans, restr_source
|
single 📖 | CompOp | 4 mathmath: single_target, single_apply, single_symm_apply, single_source
|
source 📖 | CompOp | 346 mathmath: Unitary.openPartialHomeomorph_source, trans_target'', FiberPrebundle.mem_pretrivializationAt_source, Trivialization.pullback_source, OpenPartialHomeomorph.bijOn, exists_mem_target, SmoothPartitionOfUnity.exists_isSubordinate_chartAt_source, OpenPartialHomeomorph.isOpen_extend_preimage, OpenPartialHomeomorph.restr_inter_source, Trivialization.domExtend_source, isOpen_extChartAt_preimage', mdifferentiableOn_iff, PartialDiffeomorph.contMDiffOn, OpenPartialHomeomorph.symm_image_target_eq_source, trans_source, Manifold.LiftSourceTargetPropertyAt.mem_domChart_source, ChartedSpaceCore.continuousOn_toFun, OpenPartialHomeomorph.transHomeomorph_source, piecewise_source, OpenPartialHomeomorph.IsImage.preimage_eq', contMDiffOn_chart, mdifferentiable_iff_target, Manifold.LocalPresentationAt.mem_codChart_source, Trivialization.codExtend_source, OpenPartialHomeomorph.image_trans_source, ImplicitFunctionData.pt_mem_toPartialHomeomorph_source, Topology.IsOpenEmbedding.toOpenPartialHomeomorph_source, OpenPartialHomeomorph.EqOnSource.source_eq, ContinuousWithinAt.extChartAt_symm_preimage_inter_range_eventuallyEq, OpenPartialHomeomorph.ofSet_source, mem_chart_source, Equidecomp.map_target, OpenPartialHomeomorph.ofSet_trans', OpenPartialHomeomorph.restr_source_inter, mdifferentiableOn_extChartAt, map_target, Manifold.IsImmersionAt.mem_domChart_source, OpenPartialHomeomorph.ext_iff, IsLocalHomeomorphOn.OpenPartialHomeomorph.isLocalHomeomorphOn, OpenPartialHomeomorph.EqOnSource.eqOn, FiberPrebundle.continuous_trivChange, OpenPartialHomeomorph.trans_source', OpenPartialHomeomorph.preimage_interior, stereographic'_source, SmoothBumpCovering.mem_extChartAt_source_of_eq_one, chart_source_mem_nhds, OpenPartialHomeomorph.symm_mapsTo, Topology.RelCWComplex.source_eq, OpenPartialHomeomorph.open_source, Trivialization.eqOn, PartialDiffeomorph.contMDiffOn_toFun, Circle.argPartialEquiv_source, FiberBundleCore.mk_mem_localTrivAt_source, OpenPartialHomeomorph.isOpen_extend_source, symm_image_target_eq_source, FiberBundleCore.mem_localTrivAt_source, OpenPartialHomeomorph.self_trans_symm, SmoothBumpFunction.exists_r_pos_lt_subset_ball, Trivialization.continuousOn, OpenPartialHomeomorph.source_inter_preimage_inv_preimage, injOn, OpenPartialHomeomorph.isLocalStructomorphWithinAt_source_iff, OpenPartialHomeomorph.lift_openEmbedding_source, Manifold.LocalPresentationAt.mem_domChart_source, Pretrivialization.proj_surjOn_baseSet, ModelWithCorners.source_eq, trans_target', Equidecomp.isDecompOn', ImplicitFunctionData.pt_mem_toOpenPartialHomeomorph_source, OpenPartialHomeomorph.toHomeomorphSourceTarget_apply_coe, IsImage.iff_preimage_eq, OpenPartialHomeomorph.restrOpen_source, HasStrictFDerivAt.mem_toOpenPartialHomeomorph_source, continuousOn_tangentCoordChange, iUnion_source_chartAt, refl_restr_source, mdifferentiableOn_iff_target, IsImage.image_eq, trans_source'', Trivialization.restrictPreimage'_source, ModelWithCorners.ext_iff, SmoothBumpFunction.support_eq_inter_preimage, OpenPartialHomeomorph.trans_source'', Manifold.IsImmersionAtOfComplement.mem_domChart_source, OpenPartialHomeomorph.pi_source, Manifold.IsImmersionAt.mem_codChart_source, FiberBundleCore.mem_localTrivAsPartialEquiv_source, symm_image_target_inter_eq, image_source_eq_target, IsLocalDiffeomorphAt.localInverse_contMDiffOn, bijOn, NumberField.mixedEmbedding.polarCoordReal_source, Equiv.transPartialEquiv_source, image_trans_source, prod_source, OpenPartialHomeomorph.contDiffOn_extend_coord_change, OpenPartialHomeomorph.isOpen_image_source_inter, OpenPartialHomeomorph.inv_image_trans_target, OpenPartialHomeomorph.leftInvOn, trans_source', trans_refl_restr', Manifold.LocalPresentationAt.source_subset_preimage_source, OpenPartialHomeomorph.restr_source', IsImage.leftInvOn_piecewise, FiberwiseLinear.source_trans_PartialHomeomorph, VectorBundleCore.mem_trivChange_source, source_restr_subset_source, continuousOn_extChartAt, IsImage.symm_mapsTo, ModelWithCorners.prod_source, Pretrivialization.codExtend_source, SmoothBumpFunction.tsupport_subset_chartAt_source, Pretrivialization.source_eq, OpenPartialHomeomorph.symm_image_target_inter_eq, HasStrictFDerivAt.mem_implicitToOpenPartialHomeomorphOfComplemented_source, contMDiff_iff_target, SmoothBumpFunction.eqOn_source, Trivialization.map_target, contMDiffOn_extChartAt, EqOnSource.source_eq, OpenPartialHomeomorph.isOpenEmbedding_restrict, OpenPartialHomeomorph.IsImage.iff_preimage_eq', OpenPartialHomeomorph.preimage_frontier, Trivialization.preimage_subset_source, Trivialization.proj_surjOn_baseSet, target_subset_preimage_source, OpenPartialHomeomorph.image_source_eq_target, isOpen_extChartAt_preimage, MeasureTheory.integral_target_eq_integral_abs_det_fderiv_smul, FiberBundleCore.mem_localTriv_source, IsImage.mapsTo, mdifferentiable_iff, isOpen_extChartAt_source, VectorBundleCore.mem_source_at, OpenPartialHomeomorph.refl_source, IsLocalDiffeomorphAt.contmdiffOn_localInverse, map_source'', extChartAt_source, Topology.CWComplex.source_eq, Set.BijOn.toPartialEquiv_source, TangentBundle.trivializationAt_source, Trivialization.coe_mem_source, OpenPartialHomeomorph.image_source_inter_eq, ext_coord_change_source, OpenPartialHomeomorph.univUnitBall_source, Manifold.IsImmersionAtOfComplement.source_subset_preimage_source, mem_extChartAt_source, FiberPrebundle.isOpen_target_of_mem_pretrivializationAtlas_inter, isLocalStructomorphOn_contDiffGroupoid_iff, ChartedSpace.mem_chart_source, source_inter_preimage_inv_preimage, SmoothBumpCovering.mem_chartAt_ind_source, EqOnSource.source_inter_preimage_eq, IsLocalDiffeomorphAt.localInverse_open_source, contMDiffOn_of_mem_contDiffGroupoid, ContinuousWithinAt.nhdsWithin_extChartAt_symm_preimage_inter_range, isImage_source_target, ChartedSpaceCore.mem_chart_source, OpenPartialHomeomorph.symm_target, OpenPartialHomeomorph.extend_image_source_inter, Trivialization.mem_source, extChartAt_source_mem_nhds, OpenPartialHomeomorph.map_target, StructureGroupoid.LocalInvariantProp.liftPropOn_of_mem_groupoid, OpenPartialHomeomorph.restrContDiff_source, Trivialization.source_inter_preimage_target_inter, NumberField.mixedEmbedding.polarCoord_source, IsLocalDiffeomorphAt.localInverse_eqOn_right, symm_image_target_inter_eq', mem_achart_source, StructureGroupoid.LocalInvariantProp.liftPropOn_of_mem_maximalAtlas, Manifold.IsImmersionAt.source_subset_preimage_source, contDiffOn_fderiv_coord_change, OpenPartialHomeomorph.IsImage.mapsTo, OpenPartialHomeomorph.surjOn, AddCircle.openPartialHomeomorphCoe_source, Pretrivialization.coe_mem_source, Pretrivialization.restrictPreimage_source, OpenPartialHomeomorph.contDiffOn_restrContDiff_source, symm_source, OpenPartialHomeomorph.IsImage.isOpen_iff, Trivialization.proj_clift, OpenPartialHomeomorph.isImage_source_target, ChartedSpace.isOpen_iff, symm_mapsTo, Homeomorph.toOpenPartialHomeomorphOfImageEq_source, single_source, OpenPartialHomeomorph.IsImage.symm_mapsTo, contMDiffWithinAt_iff', OpenPartialHomeomorph.isOpen_extend_preimage', SmoothPartitionOfUnity.exists_isSubordinate_chartAt_source_of_isClosed, Complex.polarCoord_source, image_source_inter_eq', IsImage.symm_image_eq, OpenPartialHomeomorph.image_source_inter_eq', PartialDiffeomorph.mdifferentiableOn, Pretrivialization.mem_source, FiberPrebundle.isOpen_source, OpenPartialHomeomorph.trans_source, OpenPartialHomeomorph.IsImage.leftInvOn_piecewise, IsOpen.trivializationDiscrete_source, VectorPrebundle.mem_trivialization_at_source, OpenPartialHomeomorph.trans_target', OpenPartialHomeomorph.secondCountableTopology_source, contMDiffOn_iff, mdifferentiableOn_atlas, UniqueMDiffOn.uniqueDiffOn_inter_preimage, mdifferentiableWithinAt_iff_target_inter', OpenPartialHomeomorph.isOpen_inter_preimage, contMDiff_iff, FiberBundleCore.localTrivAsPartialEquiv_source, StructureGroupoid.LocalInvariantProp.liftPropOn_chart, refl_source, SmoothBumpCovering.mem_extChartAt_ind_source, symm_target, contDiffOn_ext_coord_change, Equidecomp.isDecompOn, symm_image_eq_source_inter_preimage, OpenPartialHomeomorph.symm_image_eq_source_inter_preimage, TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe_source, OpenPartialHomeomorph.continuousOn, stereographic_source, hom_trivializationAt_source, extChartAt_source_mem_nhdsWithin, source_subset_preimage_target, Pretrivialization.trans_source, SmoothBumpFunction.coe_def, tangentBundleCore_baseSet, FiberBundle.mem_trivializationAt_proj_source, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_iff, OpenPartialHomeomorph.extend_source, OpenPartialHomeomorph.unitBallBall_source, Manifold.IsImmersionAtOfComplement.mem_codChart_source, Topology.IsQuotientMap.trivializationOfVAddDisjoint_source, OpenPartialHomeomorph.restr_source, ofSet_source, tangentBundleCore_localTriv_baseSet, ext_iff, Trivialization.restrictPreimage_source, OpenPartialHomeomorph.IsImage.image_eq, IsImage.restr_source, OpenPartialHomeomorph.preimage_closure, OpenPartialHomeomorph.injOn, image_source_inter_eq, NumberField.mixedEmbedding.fundamentalCone.expMap_source, Trivialization.continuousOn_proj, OpenPartialHomeomorph.trans_of_set', Manifold.LiftSourceTargetPropertyAt.mem_codChart_source, pi_source, TangentBundle.trivializationAt_baseSet, OpenPartialHomeomorph.IsImage.symm_image_eq, HasStrictFDerivAt.mem_implicitToPartialHomeomorphOfComplemented_source, Pretrivialization.restrictPreimage'_source, contMDiffOn_of_mem_maximalAtlas, map_extChartAt_nhdsWithin_eq_image, Trivialization.sourceHomeomorphBaseSetProd_symm_apply, ChartedSpaceCore.open_source, Equiv.toPartialEquivOfImageEq_source, Trivialization.symm_trans_source_eq, OpenPartialHomeomorph.lift_openEmbedding_symm_target, OpenPartialHomeomorph.continuousOn_toFun, ContMDiffFiberwiseLinear.locality_aux₁, polarCoord_source_ae_eq_univ, Pretrivialization.eqOn, Homeomorph.transOpenPartialHomeomorph_source, VectorBundleCore.mem_localTriv_source, ContDiffAt.mem_toPartialHomeomorph_source, SmoothBumpFunction.tsupport_subset_extChartAt_source, OpenPartialHomeomorph.symm_source, OpenPartialHomeomorph.invOn, OpenPartialHomeomorph.IsImage.iff_symm_preimage_eq', Equiv.toPartialEquiv_source, OpenPartialHomeomorph.map_source'', leftInvOn, IsLocalDiffeomorphAt.localInverse_mem_source, OpenPartialHomeomorph.mapsTo, OpenPartialHomeomorph.prod_source, NumberField.mixedEmbedding.polarSpaceCoord_source, inv_image_trans_target, Topology.IsQuotientMap.trivializationOfSMulDisjoint_source, OpenPartialHomeomorph.source_preimage_target, OpenPartialHomeomorph.IsImage.preimage_eq, VectorPrebundle.totalSpaceMk_preimage_source, IsImage.preimage_eq, Real.cosPartialEquiv_source, Equidecomp.restr_source, ApproximatesLinearOn.toPartialHomeomorph_source, HasStrictFDerivAt.mem_implicitToPartialHomeomorph_source, Homeomorph.toOpenPartialHomeomorph_source, Trivialization.sourceHomeomorphBaseSetProd_apply, OpenPartialHomeomorph.continuousOn_extend, Real.expPartialHomeomorph_source, OpenPartialHomeomorph.lift_openEmbedding_symm_source, SmoothBumpFunction.support_subset_source, ContDiffAt.mem_toOpenPartialHomeomorph_source, OpenPartialHomeomorph.IsImage.symm_preimage_eq', mapsTo, PartialDiffeomorph.open_source, ModelWithCorners.uniqueDiffOn_preimage_source, self_trans_symm, OpenPartialHomeomorph.extend_coord_change_source, ChartedSpaceCore.open_source', contMDiffOn_iff_target, Trivialization.frontier_preimage, OpenPartialHomeomorph.subtypeRestr_source, Pretrivialization.codExtend'_source, Trivialization.codExtend'_source, EqOnSource.eqOn, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_source, surjOn, ApproximatesLinearOn.toOpenPartialHomeomorph_source, Units.chartAt_source, FiberwiseLinear.source_trans_openPartialHomeomorph, FiberPrebundle.totalSpaceMk_preimage_source, map_target', OpenPartialHomeomorph.continuousOn_iff_continuousOn_comp_right, source_inter_preimage_target_inter, Pretrivialization.domExtend_source, OpenPartialHomeomorph.const_source, NumberField.mixedEmbedding.fundamentalCone.expMap_single_source, invOn, Trivialization.contMDiffOn, Pretrivialization.symm_trans_source_eq, Bundle.Trivial.trivialization_source, TopologicalSpace.Opens.partialHomeomorphSubtypeCoe_source, polarCoord_source, Pretrivialization.target_inter_preimage_symm_source_eq, Trivialization.prod_source, HasStrictFDerivAt.mem_implicitToOpenPartialHomeomorph_source, StructureGroupoid.restriction_mem_maximalAtlas_subtype, HasStrictFDerivAt.mem_toPartialHomeomorph_source, restr_source, FiberBundleCore.open_source', SmoothBumpCovering.mem_chartAt_source_of_eq_one, OpenPartialHomeomorph.trans_target'', OpenPartialHomeomorph.source_inter_preimage_target_inter, OpenPartialHomeomorph.toHomeomorphSourceTarget_symm_apply_coe, TangentBundle.mem_chart_source_iff, Manifold.LiftSourceTargetPropertyAt.source_subset_preimage_source, TangentBundle.trivializationAt_target, mem_groupoid_of_pregroupoid, OpenPartialHomeomorph.IsImage.iff_preimage_eq, transEquiv_source, FiberBundleCore.mem_trivChange_source, OpenPartialHomeomorph.univBall_source, Trivialization.source_eq
|
target 📖 | CompOp | 314 mathmath: restr_target, trans_target'', NumberField.mixedEmbedding.integral_comp_polarSpaceCoord_symm, single_target, Homeomorph.toOpenPartialHomeomorph_target, OpenPartialHomeomorph.bijOn, exists_mem_target, NumberField.mixedEmbedding.lintegral_comp_polarCoord_symm, ApproximatesLinearOn.toPartialHomeomorph_target, OpenPartialHomeomorph.map_subtype_source, UniqueMDiffOn.uniqueMDiffOn_preimage, OpenPartialHomeomorph.subtypeRestr_symm_trans_subtypeRestr, OpenPartialHomeomorph.restr_target, Manifold.IsImmersionAtOfComplement.target_subset_preimage_target, Manifold.IsImmersionAt.map_target_subset_target, Complex.integral_comp_pi_polarCoord_symm, IsOpen.trivializationDiscrete_target, mdifferentiableOn_iff, OpenPartialHomeomorph.symm_image_target_eq_source, OpenPartialHomeomorph.IsImage.preimage_eq', chart_target_mem_nhds, OpenPartialHomeomorph.image_eq_target_inter_inv_preimage, OpenPartialHomeomorph.image_trans_source, Pretrivialization.target_eq, ImplicitFunctionData.map_pt_mem_toOpenPartialHomeomorph_target, extChartAt_target_eventuallyEq, Topology.RelCWComplex.continuousOn_symm, ContinuousWithinAt.extChartAt_symm_preimage_inter_range_eventuallyEq, UniqueMDiffWithinAt.preimage_PartialHomeomorph, Pretrivialization.restrictPreimage_target, OpenPartialHomeomorph.IsImage.inter_eq_of_inter_eq_of_eqOn, OpenPartialHomeomorph.transHomeomorph_target, mdifferentiableWithinAt_iff_target_inter, FiberPrebundle.continuous_trivChange, VectorBundleCore.mem_localTriv_target, pi_target, isOpen_extChartAt_target, Equiv.transPartialEquiv_target, OpenPartialHomeomorph.extend_target_mem_nhdsWithin, OpenPartialHomeomorph.trans_source', IsImage.inter_eq_of_inter_eq_of_eqOn, IsImage.iff_symm_preimage_eq, Trivialization.pullback_target, FiberPrebundle.continuous_symm_of_mem_pretrivializationAtlas, contMDiffOn_chart_symm, Trivialization.contMDiffOn_symm_trans, map_source', Homeomorph.toOpenPartialHomeomorphOfImageEq_target, OpenPartialHomeomorph.symm_mapsTo, NumberField.mixedEmbedding.polarSpaceCoord_target, symm_image_target_eq_source, Real.cosPartialEquiv_target, NumberField.mixedEmbedding.fundamentalCone.expMap_target, Manifold.IsImmersionAtOfComplement.map_target_subset_target, ImplicitFunctionData.map_pt_mem_toPartialHomeomorph_target, ModelWithCorners.prod_target, Complex.integral_comp_polarCoord_symm, HasStrictFDerivAt.mem_implicitToPartialHomeomorphOfComplemented_target, trans_target', OpenPartialHomeomorph.pi_target, symm_trans_self, extChartAt_target_mem_nhdsWithin, FiberBundleCore.localTrivAsPartialEquiv_target, image_eq_target_inter_inv_preimage, UniqueMDiffOn.uniqueDiffOn_target_inter, OpenPartialHomeomorph.toHomeomorphSourceTarget_apply_coe, Pretrivialization.restrictPreimage'_target, refl_restr_target, Trivialization.target_eq, lintegral_comp_pi_polarCoord_symm, IsImage.image_eq, ContDiffAt.image_mem_toOpenPartialHomeomorph_target, trans_source'', polarCoord_target, TopologicalSpace.Opens.partialHomeomorphSubtypeCoe_target, HasStrictFDerivAt.mem_implicitToOpenPartialHomeomorphOfComplemented_target, OpenPartialHomeomorph.extend_image_target_mem_nhds, Bundle.Trivial.trivialization_target, ModelWithCorners.ext_iff, Pretrivialization.preimage_symm_proj_baseSet, UniqueMDiffOn.uniqueMDiffOn_target_inter, OpenPartialHomeomorph.trans_source'', transEquiv_target, Manifold.IsImmersionAt.writtenInCharts, symm_image_target_inter_eq, image_source_eq_target, OpenPartialHomeomorph.target_inter_inv_preimage_preimage, bijOn, OpenPartialHomeomorph.prod_target, stereographic'_target, image_trans_source, IsImage.symm_preimage_eq, Pretrivialization.codExtend_target, OpenPartialHomeomorph.inv_image_trans_target, trans_source', mem_extChartAt_target, map_source, extChartAt_mem_closure_interior, measurableSet_pi_polarCoord_target, integral_comp_polarCoord_symm, OpenPartialHomeomorph.extend_target, OpenPartialHomeomorph.EqOnSource.target_eq, EqOnSource.symm_eqOn, IsImage.symm_mapsTo, contMDiffWithinAt_iff_of_mem_source', OpenPartialHomeomorph.symm_image_target_inter_eq, SmoothBumpFunction.ball_subset, IsLocalDiffeomorphAt.localInverse_mem_target, mdifferentiableOn_extChartAt_symm, OpenPartialHomeomorph.continuousOn_extend_symm, OpenPartialHomeomorph.symm_trans_self, OpenPartialHomeomorph.IsImage.iff_preimage_eq', target_subset_preimage_source, HasStrictFDerivAt.mem_implicitToOpenPartialHomeomorph_target, OpenPartialHomeomorph.image_source_eq_target, OpenPartialHomeomorph.univUnitBall_target, MeasureTheory.integral_target_eq_integral_abs_det_fderiv_smul, IsImage.mapsTo, mdifferentiable_iff, ModelWithCorners.range_eq_target, OpenPartialHomeomorph.restrContDiff_target, contMDiffOn_extChartAt_symm, extChartAt_target_mem_nhdsWithin', UniqueMDiffWithinAt.preimage_openPartialHomeomorph, Trivialization.mem_target, map_source'', FiberBundleCore.mem_localTrivAt_target, OpenPartialHomeomorph.extend_symm_preimage_inter_range_eventuallyEq_aux, OpenPartialHomeomorph.image_source_inter_eq, Trivialization.codExtend'_target, FiberPrebundle.isOpen_target_of_mem_pretrivializationAtlas_inter, isLocalStructomorphOn_contDiffGroupoid_iff, OpenPartialHomeomorph.unitBallBall_target, piecewise_target, ContinuousWithinAt.nhdsWithin_extChartAt_symm_preimage_inter_range, isImage_source_target, FiberBundleCore.mem_localTriv_target, OpenPartialHomeomorph.symm_target, extChartAt_target_eventuallyEq', Set.BijOn.toPartialEquiv_target, Complex.lintegral_comp_polarCoord_symm, target_subset_range, Trivialization.source_inter_preimage_target_inter, symm_image_target_inter_eq', OpenPartialHomeomorph.continuousOn_invFun, ofSet_target, Unitary.openPartialHomeomorph_target, Pretrivialization.symm_trans_target_eq, OpenPartialHomeomorph.IsImage.mapsTo, OpenPartialHomeomorph.surjOn, extChartAt_target_subset_range, Pretrivialization.mem_target, symm_source, OpenPartialHomeomorph.IsImage.symm_eqOn_of_inter_eq_of_eqOn, OpenPartialHomeomorph.extend_target_eventuallyEq, OpenPartialHomeomorph.IsImage.isOpen_iff, TangentBundle.mem_chart_target_iff, ModelWithCorners.target_eq, FiberwiseLinear.target_trans_openPartialHomeomorph, TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe_target, OpenPartialHomeomorph.isImage_source_target, NumberField.mixedEmbedding.polarCoord_target, OpenPartialHomeomorph.extend_target', symm_mapsTo, OpenPartialHomeomorph.IsImage.symm_mapsTo, contMDiffWithinAt_iff', ContDiffAt.image_mem_toPartialHomeomorph_target, Trivialization.symm_trans_target_eq, image_source_inter_eq', uniqueMDiffWithinAt_iff, IsImage.symm_image_eq, OpenPartialHomeomorph.image_source_inter_eq', NumberField.mixedEmbedding.polarSpaceCoord_target', stereographic_target, OpenPartialHomeomorph.trans_target', contMDiffOn_iff, Pretrivialization.open_target, OpenPartialHomeomorph.map_source, UniqueMDiffOn.uniqueDiffOn_inter_preimage, mdifferentiableWithinAt_iff_target_inter', Trivialization.restrictPreimage'_target, Topology.IsOpenEmbedding.toOpenPartialHomeomorph_target, contMDiffWithinAt_extChartAt_symm_target_self, OpenPartialHomeomorph.symm_trans_restr, contMDiff_iff, Equiv.toPartialEquivOfImageEq_target, continuousOn_extChartAt_symm, OpenPartialHomeomorph.IsImage.iff_symm_preimage_eq, symm_target, OpenPartialHomeomorph.EqOnSource.symm_eqOn_target, mdifferentiableWithinAt_iff_of_mem_source', VectorField.contMDiffWithinAt_mpullbackWithin_extChartAt_symm, source_subset_preimage_target, OpenPartialHomeomorph.interior_extend_target_subset_interior_range, Trivialization.domExtend_target, Trivialization.prod_target, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_iff, FiberBundle.extChartAt_target, FiberBundleCore.mem_localTrivAsPartialEquiv_target, OpenPartialHomeomorph.refl_target, OpenPartialHomeomorph.contDiffOn_restrContDiff_target, OpenPartialHomeomorph.lift_openEmbedding_target, FiberwiseLinear.target_trans_PartialHomeomorph, Manifold.IsImmersionAt.target_subset_preimage_target, ApproximatesLinearOn.closedBall_subset_target, OpenPartialHomeomorph.IsImage.image_eq, image_source_inter_eq, OpenPartialHomeomorph.subtypeRestr_symm_eqOn, NumberField.mixedEmbedding.lintegral_comp_polarCoordReal_symm, Topology.IsQuotientMap.trivializationOfSMulDisjoint_target, HasStrictFDerivAt.image_mem_toPartialHomeomorph_target, OpenPartialHomeomorph.nhdsWithin_extend_target_eq, nhdsWithin_extChartAt_target_eq, Equidecomp.apply_mem_target, injOn_pi_polarCoord_symm, OpenPartialHomeomorph.subtypeRestr_target_subset, OpenPartialHomeomorph.const_target, ModelWithCorners.isInteriorPoint_iff, Homeomorph.transOpenPartialHomeomorph_target, OpenPartialHomeomorph.rightInvOn, OpenPartialHomeomorph.IsImage.symm_image_eq, Pretrivialization.codExtend'_target, lintegral_comp_polarCoord_symm, interior_extChartAt_target_nonempty, Manifold.IsImmersionAtOfComplement.writtenInCharts, OpenPartialHomeomorph.subtypeRestr_symm_eqOn_of_le, OpenPartialHomeomorph.isOpen_extend_target, Equiv.toPartialEquiv_target, ApproximatesLinearOn.toOpenPartialHomeomorph_target, NumberField.mixedEmbedding.polarCoordReal_symm_target_ae_eq_univ, Circle.argPartialEquiv_target, OpenPartialHomeomorph.lift_openEmbedding_symm_target, PartialDiffeomorph.contMDiffOn_invFun, contMDiffOn_extend_symm, OpenPartialHomeomorph.symm_source, OpenPartialHomeomorph.invOn, OpenPartialHomeomorph.IsImage.iff_symm_preimage_eq', Trivialization.mk_mem_target, OpenPartialHomeomorph.map_source'', extChartAt_target, Trivialization.contMDiffOn_symm, StructureGroupoid.LocalInvariantProp.liftPropOn_symm_of_mem_maximalAtlas, IsImage.restr_target, OpenPartialHomeomorph.mapsTo, EqOnSource.target_eq, OpenPartialHomeomorph.continuousOn_symm, Trivialization.codExtend_target, Complex.lintegral_comp_pi_polarCoord_symm, OpenPartialHomeomorph.ofSet_target, inv_image_trans_target, OpenPartialHomeomorph.source_preimage_target, NumberField.mixedEmbedding.polarCoord_target_eq_polarCoordReal_target, pi_polarCoord_symm_target_ae_eq_univ, OpenPartialHomeomorph.preimage_eventuallyEq_target_inter_preimage_inter, IsImage.symm_eq_on_of_inter_eq_of_eqOn, OpenPartialHomeomorph.ball_subset_univBall_target, OpenPartialHomeomorph.extend_target_subset_range, HasStrictFDerivAt.mem_implicitToPartialHomeomorph_target, ChartedSpaceCore.open_target, OpenPartialHomeomorph.lift_openEmbedding_symm_source, OpenPartialHomeomorph.isOpen_inter_preimage_symm, PartialDiffeomorph.open_target, target_inter_inv_preimage_preimage, Real.expPartialHomeomorph_target, OpenPartialHomeomorph.open_target, refl_target, trans_target, VectorField.eventually_contMDiffWithinAt_mpullbackWithin_extChartAt_symm, Topology.IsQuotientMap.trivializationOfVAddDisjoint_target, OpenPartialHomeomorph.IsImage.symm_preimage_eq', mapsTo, StructureGroupoid.LocalInvariantProp.liftPropOn_chart_symm, NumberField.mixedEmbedding.polarCoordReal_target, Complex.polarCoord_target, contMDiffOn_symm_of_mem_maximalAtlas, OpenPartialHomeomorph.univBall_target, uniqueDiffOn_extChartAt_target, extChartAt_target_mem_nhds, mem_chart_target, surjOn, NumberField.mixedEmbedding.integral_comp_polarCoord_symm, Topology.CWComplex.continuousOn_symm, uniqueDiffWithinAt_extChartAt_target, OpenPartialHomeomorph.IsImage.symm_preimage_eq, Pretrivialization.mk_mem_target, source_inter_preimage_target_inter, OpenPartialHomeomorph.trans_target, HasStrictFDerivAt.image_mem_toOpenPartialHomeomorph_target, invOn, Equidecomp.restr_target, mdifferentiableOn_atlas_symm, IsLocalDiffeomorphAt.localInverse_eqOn_left, NumberField.mixedEmbedding.integral_comp_polarCoordReal_symm, hom_trivializationAt_target, integral_comp_pi_polarCoord_symm, Pretrivialization.target_inter_preimage_symm_source_eq, rightInvOn, prod_target, StructureGroupoid.restriction_mem_maximalAtlas_subtype, AddCircle.openPartialHomeomorphCoe_target, OpenPartialHomeomorph.trans_target'', NumberField.mixedEmbedding.fundamentalCone.expMap_single_target, nhdsWithin_extChartAt_target_eq', OpenPartialHomeomorph.source_inter_preimage_target_inter, Pretrivialization.domExtend_target, OpenPartialHomeomorph.toHomeomorphSourceTarget_symm_apply_coe, TangentBundle.trivializationAt_target, extChartAt_target_subset_closure_interior, mem_groupoid_of_pregroupoid, SmoothBumpFunction.closedBall_subset, Trivialization.restrictPreimage_target, SmoothBumpFunction.ball_inter_range_eq_ball_inter_target, ModelWithCorners.extChartAt_transContinuousLinearEquiv_target, NumberField.mixedEmbedding.lintegral_comp_polarSpaceCoord_symm
|
toEquiv 📖 | CompOp | — |
toFun 📖 | CompOp | 443 mathmath: restr_target, trans_target'', OpenPartialHomeomorph.map_extend_nhdsWithin_eq_image, IsLocalDiffeomorphAt.localInverse_eventuallyEq_right, exists_mem_target, contMDiffAt_extend, contMDiffAt_iff_of_mem_source, OpenPartialHomeomorph.extend_preimage_inter_eq, contMDiffWithinAt_iff_target, OpenPartialHomeomorph.isOpen_extend_preimage, SmoothBumpFunction.support_eq_symm_image, extChartAt_to_inv, OpenPartialHomeomorph.map_extend_nhds_of_boundaryless, isOpen_extChartAt_preimage', ApproximatesLinearOn.inverse_continuousOn, Pretrivialization.preimage_symm_proj_inter, MDifferentiableWithinAt.differentiableWithinAt_mpullbackWithin_vectorField, SmoothBumpFunction.rOut_pos, mdifferentiableOn_iff, PartialDiffeomorph.contMDiffOn, right_inv', trans_source, mdifferentiableWithinAt_iff_of_mem_maximalAtlas, ModelWithCorners.symm_continuousWithinAt_comp_right_iff, ChartedSpaceCore.continuousOn_toFun, trans_apply, mdifferentiable_iff_target, contMDiffAt_iff_source, eventually_enorm_mfderivWithin_symm_extChartAt_lt, extChartAt_target_eventuallyEq, Equidecomp.restr_invFun, TangentBundle.symmL_trivializationAt, Topology.RelCWComplex.continuousOn_symm, ContinuousWithinAt.extChartAt_symm_preimage_inter_range_eventuallyEq, map_extChartAt_symm_nhdsWithin, Topology.CWComplex.continuousOn, Equidecomp.map_target, mdifferentiableOn_extChartAt, map_target, eq_symm_apply, OpenPartialHomeomorph.tendsto_extend_comp_iff, OpenPartialHomeomorph.map_extend_nhdsWithin_eq_image_of_subset, mdifferentiableWithinAt_iff_target_inter, ModelWithCorners.mdifferentiableOn_symm, contMDiffWithinAt_iff_image, tangentCoordChange_def, ModelWithCorners.image_eq, disjointUnion_apply, map_extChartAt_symm_nhdsWithin', continuousAt_extChartAt, Topology.RelCWComplex.pairwiseDisjoint', FiberPrebundle.continuous_trivChange, hasMFDerivAt_extChartAt, OpenPartialHomeomorph.extend_target_mem_nhdsWithin, OpenPartialHomeomorph.coe_coe, Equiv.toPartialEquiv_apply, map_extChartAt_symm_nhdsWithin_range', modelWithCornersSelf_coe_symm, IsImage.iff_symm_preimage_eq, extChartAt_preimage_inter_eq, FiberPrebundle.continuous_symm_of_mem_pretrivializationAtlas, map_extChartAt_symm_nhdsWithin_range, extChartAt_inl_apply, map_extChartAt_nhdsWithin', IsLocalDiffeomorphAt.localInverse_mdifferentiableAt, map_source', inTangentCoordinates_eq_mfderiv_comp, mdifferentiableAt_iff, Equiv.transPartialEquiv_symm_apply, PartialDiffeomorph.contMDiffOn_toFun, symm_image_target_eq_source, single_apply, Topology.RelCWComplex.continuousOn, MDifferentiableWithinAt.differentiableWithinAt_writtenInExtChartAt, OpenPartialHomeomorph.continuousAt_extend_symm', transEquiv_symm_apply, Topology.RelCWComplex.union', SmoothBumpFunction.exists_r_pos_lt_subset_ball, PartialDiffeomorph.isLocalDiffeomorphAt, IsImage.restr_symm_apply, IsMIntegralCurveOn.hasDerivWithinAt, injOn, extChartAt_preimage_mem_nhdsWithin', Equiv.toPartialEquiv_symm_apply, IccLeftChart_extend_interior_pos, trans_target', ModelWithCorners.uniqueDiffOn_preimage, Equidecomp.isDecompOn', extChartAt_target_mem_nhdsWithin, eventually_norm_mfderivWithin_symm_extChartAt_lt, image_eq_target_inter_inv_preimage, UniqueMDiffOn.uniqueDiffOn_target_inter, IsImage.iff_preimage_eq, extChartAt_self_apply, mapsTo_extChartAt, ModelWithCorners.symm_comp_self, preimage_extChartAt_eventuallyEq_compl_singleton, mdifferentiableOn_iff_target, IsImage.image_eq, trans_source'', OpenPartialHomeomorph.extend_image_target_mem_nhds, hasMFDerivWithinAt_extChartAt, Pretrivialization.mk_symm, Real.cosPartialEquiv_apply, OpenPartialHomeomorph.toFun_eq_coe, ModelWithCorners.ext_iff, Pretrivialization.preimage_symm_proj_baseSet, UniqueMDiffOn.uniqueMDiffOn_target_inter, contMDiffAt_iff_source_of_mem_source, SmoothBumpFunction.support_eq_inter_preimage, FiberBundleCore.localTrivAsPartialEquiv_coe, Manifold.IsImmersionAt.writtenInCharts, Pretrivialization.restrictPreimage_toFun, symm_image_target_inter_eq, image_source_eq_target, SmoothBumpFunction.tsupport_subset_symm_image_closedBall, MDifferentiableAt.differentiableWithinAt_writtenInExtChartAt, IsLocalDiffeomorphAt.localInverse_contMDiffOn, bijOn, image_trans_source, Trivialization.domExtend_symm_apply, TangentBundle.trivializationAt_apply, prod_coe_symm, IsImage.symm_preimage_eq, OpenPartialHomeomorph.contDiffOn_extend_coord_change, trans_refl_restr, trans_source', OpenPartialHomeomorph.continuousWithinAt_writtenInExtend_iff, trans_refl_restr', Trivialization.prod_symm_apply, Equiv.toPartialEquivOfImageEq_symm_apply, OpenPartialHomeomorph.continuousAt_extend, mem_extChartAt_target, mem_symm_trans_source, map_source, OpenPartialHomeomorph.map_extend_symm_nhdsWithin, IsImage.leftInvOn_piecewise, extChartAt_mem_closure_interior, mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm, ModelWithCorners.toPartialEquiv_coe, map_extChartAt_nhds_of_boundaryless, ModelWithCorners.prod_symm_apply, restr_coe_symm, extChartAt_preimage_mem_nhds, OpenPartialHomeomorph.extend_target, piecewise_apply, EqOnSource.symm_eqOn, extChartAt_self_eq, continuousOn_extChartAt, IsImage.restr_apply, IsImage.symm_mapsTo, invFun_as_coe, OpenPartialHomeomorph.contDiffWithinAt_extend_coord_change', contMDiffWithinAt_iff_of_mem_source', mdifferentiableWithinAt_iff_image, OpenPartialHomeomorph.extend_coord_change_source_mem_nhdsWithin', SmoothBumpFunction.ball_subset, injective_symm_of_target_eq_univ, contMDiff_iff_target, mdifferentiableOn_extChartAt_symm, SmoothBumpFunction.eqOn_source, OpenPartialHomeomorph.continuousOn_extend_symm, VectorField.mlieBracketWithin_def, contMDiffOn_extChartAt, OpenPartialHomeomorph.extend_left_inv, Topology.CWComplex.union', single_symm_apply, Pretrivialization.apply_symm_apply, extChartAt_inr_apply, target_subset_preimage_source, isOpen_extChartAt_preimage, IsImage.mapsTo, mdifferentiable_iff, contMDiffAt_iff, ModelWithCorners.range_eq_target, modelWithCorners_prod_coe_symm, FiberBundleCore.localTrivAsPartialEquiv_apply, OpenPartialHomeomorph.extend_coe_symm, contMDiffOn_iff_of_mem_maximalAtlas', OpenPartialHomeomorph.map_extend_nhds, extChartAt_preimage_mem_nhdsWithin, contMDiffOn_extChartAt_symm, ModelWithCorners.symm_map_nhdsWithin_range, extChartAt_target_mem_nhdsWithin', IsLocalDiffeomorphAt.contmdiffOn_localInverse, extChartAt_preimage_mem_nhds', contMDiffWithinAt_extChartAt_symm_range_self, Pretrivialization.symm_apply, map_source'', Topology.CWComplex.pairwiseDisjoint', Pretrivialization.codExtend'_toFun, OpenPartialHomeomorph.extend_symm_preimage_inter_range_eventuallyEq_aux, OpenPartialHomeomorph.continuousOn_writtenInExtend_iff, contMDiffWithinAt_iff_target_of_mem_source, mdifferentiableOn_iff_of_subset_source, contMDiffWithinAt_iff_source_of_mem_maximalAtlas, contMDiffOn_iff_of_subset_source', Pretrivialization.symm_apply_mk_proj, ModelWithCorners.leftInverse, FiberPrebundle.isOpen_target_of_mem_pretrivializationAtlas_inter, restr_coe, Equidecomp.left_inv, MDifferentiableAt.mfderiv, source_inter_preimage_inv_preimage, EqOnSource.source_inter_preimage_eq, right_inv, Pretrivialization.proj_symm_apply', hasFDerivWithinAt_tangentCoordChange, ContinuousWithinAt.nhdsWithin_extChartAt_symm_preimage_inter_range, MDifferentiableWithinAt.mfderivWithin, Topology.CWComplex.mapsTo', contMDiffWithinAt_iff, Equiv.toPartialEquivOfImageEq_apply, OpenPartialHomeomorph.contDiffWithinAt_extend_coord_change, OpenPartialHomeomorph.extend_image_source_inter, IccLeftChart_extend_bot, extChartAt_target_eventuallyEq', piecewise_symm_apply, Pretrivialization.symm_coe_proj, target_subset_range, image_symm_image_of_subset_target, OpenPartialHomeomorph.extend_preimage_mem_nhds, SmoothBumpFunction.isClosed_image_of_isClosed, IsLocalDiffeomorphAt.localInverse_eqOn_right, symm_image_target_inter_eq', tangentBundleCore_coordChange, extChartAt_image_nhds_mem_nhds_of_boundaryless, IsImage.apply_mem_iff, contDiffOn_fderiv_coord_change, SmoothBumpFunction.isClosed_symm_image_closedBall, Topology.RelCWComplex.map_zero_mem_openCell, map_extChartAt_nhds', mdifferentiableWithinAt_iff', OpenPartialHomeomorph.extend_target_eventuallyEq, Equidecomp.right_inv, injective_of_source_eq_univ, TangentBundle.continuousLinearMapAt_trivializationAt, mdifferentiableAt_iff_target_of_mem_source, ModelWithCorners.continuous_toFun, IsLocalDiffeomorphAt.localInverse_eventuallyEq_left, ext_chart_model_space_apply, SmoothBumpFunction.eventuallyEq_of_mem_source, symm_mapsTo, contDiffWithinAtProp_self_target, writtenInExtChartAt_extChartAt, continuousAt_extChartAt_symm, ModelWithCorners.right_inv, contMDiffAt_iff_target_of_mem_source, contMDiffWithinAt_iff', IsLocalDiffeomorphAt.localInverse_isLocalDiffeomorphAt, OpenPartialHomeomorph.isOpen_extend_preimage', ModelWithCorners.coe_extChartAt_transContinuousLinearEquiv_symm, prod_coe, image_source_inter_eq', uniqueMDiffWithinAt_iff, VectorField.eventuallyEq_mpullback_mpullbackWithin_extChartAt, IsImage.symm_image_eq, map_extChartAt_nhdsWithin, ModelWithCorners.continuousOn_symm, eventually_enorm_mfderiv_extChartAt_lt, PartialDiffeomorph.mdifferentiableOn, ModelWithCorners.hasMFDerivWithinAt_symm, IccRightChart_extend_top_mem_frontier, OpenPartialHomeomorph.extend_image_nhds_mem_nhds_of_boundaryless, ModelWithCorners.continuousWithinAt_symm, Pretrivialization.coe_coe, IsLocalDiffeomorphAt.localInverse_contMDiffAt, contMDiffOn_iff, ModelWithCorners.continuous_symm, UniqueMDiffOn.uniqueDiffOn_inter_preimage, mdifferentiableWithinAt_iff_target_inter', IsLocalDiffeomorphAt.localInverse_left_inv, contMDiffOn_iff_source_of_mem_maximalAtlas, contMDiffWithinAt_extChartAt_symm_target_self, contMDiff_iff, ModelWithCorners.symm_map_nhdsWithin_image, mdifferentiableOn_iff_of_mem_maximalAtlas', uniqueMDiffWithinAt_iff_inter_range, continuousOn_extChartAt_symm, contDiffOn_ext_coord_change, writtenInExtChartAt_extChartAt_symm, Equidecomp.isDecompOn, Set.BijOn.toPartialEquiv_apply, symm_image_eq_source_inter_preimage, mdifferentiableWithinAt_iff_of_mem_source', Topology.RelCWComplex.openCell_zero_eq_singleton, VectorField.contMDiffWithinAt_mpullbackWithin_extChartAt_symm, mdifferentiableWithinAt_iff_source_of_mem_maximalAtlas, mdifferentiableWithinAt_iff, eventually_riemannianEDist_le_edist_extChartAt, contMDiffAt_extChartAt, mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm', source_subset_preimage_target, iccLeftChart_extend_zero, left_inv', coe_trans, SmoothBumpFunction.coe_def, contMDiffWithinAt_extChartAt_symm_target, FiberBundle.extChartAt_target, mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt', OpenPartialHomeomorph.extend_coe, continuousAt_extChartAt', OpenPartialHomeomorph.extend_symm_continuousWithinAt_comp_right_iff, Topology.RelCWComplex.mapsTo, contMDiffOn_iff_of_mem_maximalAtlas, ModelWithCorners.convex_range', Pretrivialization.restrictPreimage'_toFun, coe_mk, OpenPartialHomeomorph.map_extend_nhdsWithin, mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt, ext_iff, Real.cosPartialEquiv_symm_apply, IsLocalDiffeomorphAt.localInverse_right_inv, image_source_inter_eq, PartialDiffeomorph.mdifferentiableAt, contMDiffWithinAt_iff_source, Pretrivialization.symm_apply_apply, OpenPartialHomeomorph.nhdsWithin_extend_target_eq, nhdsWithin_extChartAt_target_eq, Topology.RelCWComplex.closedCell_zero_eq_singleton, Equidecomp.apply_mem_target, Topology.RelCWComplex.disjointBase', contMDiffWithinAt_iff_source_of_mem_source, contMDiffOn_iff_of_subset_source, contMDiffWithinAt_iff_of_mem_maximalAtlas, ModelWithCorners.isInteriorPoint_iff, map_extChartAt_nhdsWithin_eq_image', disjointUnion_symm_apply, mdifferentiableAt_iff_source_of_mem_source, mdifferentiableAt_iff_of_mem_source, Manifold.IsImmersionAtOfComplement.writtenInCharts, mdifferentiableWithinAt_iff_target_of_mem_source, OpenPartialHomeomorph.continuousAt_extend_symm, mdifferentiableWithinAt_extChartAt_symm, map_extChartAt_nhdsWithin_eq_image, contMDiffWithinAt_extChartAt_symm_range, contDiffWithinAt_ext_coord_change, transEquiv_apply, coe_symm_mk, eventually_norm_mfderivWithin_symm_extChartAt_comp_lt, OpenPartialHomeomorph.extend_preimage_mem_nhdsWithin, OpenPartialHomeomorph.continuousOn_toFun, Pretrivialization.continuousLinearMap_symm_apply, ofSet_coe, contMDiffOn_extend_symm, symm_image_image_of_subset_source, surjective_symm_of_source_eq_univ, Equidecomp.restr_toFun, trans'_apply, extChartAt_target, mdifferentiableWithinAt_iff_source_of_mem_source, leftInvOn, Set.BijOn.toPartialEquiv_symm_apply, ModelWithCorners.continuousAt_symm, trans_ofSet, inv_image_trans_target, isInvertible_mfderiv_extChartAt, mdifferentiableAt_iff_target, contMDiffAt_extChartAt', IsImage.preimage_eq, trans'_symm_apply, left_inv, OpenPartialHomeomorph.extend_left_inv', Equiv.transPartialEquiv_apply, extChartAt_coe_symm, ModelWithCorners.coe_extChartAt_transContinuousLinearEquiv, pi_apply, contMDiffOn_model_symm, continuousAt_extChartAt_symm'', surjective_of_target_eq_univ, OpenPartialHomeomorph.continuousOn_extend, mdifferentiableWithinAt_iff_of_mem_source, OpenPartialHomeomorph.map_extend_symm_nhdsWithin_range, isInvertible_mfderivWithin_extChartAt_symm, ModelWithCorners.coe_transContinuousLinearEquiv_symm, VectorField.mlieBracketWithin_apply, target_inter_inv_preimage_preimage, refl_coe, Topology.CWComplex.mapsTo, trans_target, Pretrivialization.proj_symm_apply, VectorField.eventually_contMDiffWithinAt_mpullbackWithin_extChartAt_symm, Pretrivialization.codExtend_toFun, mapsTo, ModelWithCorners.uniqueDiffOn_preimage_source, SmoothBumpFunction.nhdsWithin_range_basis, OpenPartialHomeomorph.coe_coe_symm, contMDiffOn_iff_target, ModelWithCorners.rightInvOn, extChartAt_target_mem_nhds, contMDiffAt_iff_target, EqOnSource.eqOn, writtenInExtChartAt_sumInr_eventuallyEq_id, surjOn, SmoothBumpCovering.embeddingPiTangent_coe, range_mem_nhds_isInteriorPoint, ModelWithCorners.nonempty_interior', ModelWithCorners.left_inv, Topology.CWComplex.continuousOn_symm, Pretrivialization.apply_symm_apply', uniqueDiffWithinAt_extChartAt_target, OpenPartialHomeomorph.extend_symm_preimage_inter_range_eventuallyEq, Circle.argPartialEquiv_symm_apply, continuousAt_extChartAt_symm', ModelWithCorners.isBoundaryPoint_iff, ModelWithCorners.mdifferentiableWithinAt_symm, source_inter_preimage_target_inter, IccRightChart_extend_top, eventually_norm_mfderiv_extChartAt_lt, invOn, IsImage.symm_apply_mem_iff, OpenPartialHomeomorph.mapsTo_extend, Equidecomp.restr_target, IsLocalDiffeomorphAt.localInverse_eqOn_left, extChartAt_coe, writtenInExtChartAt_sumInl_eventuallyEq_id, mdifferentiableOn_iff_of_mem_maximalAtlas, mdifferentiableAt_extChartAt, writtenInExtChartAt_comp, forall_mem_target, Pretrivialization.target_inter_preimage_symm_source_eq, mdifferentiableOn_iff_of_subset_source', rightInvOn, map_extChartAt_nhds, Pretrivialization.proj_toFun, IccLeftChart_extend_bot_mem_frontier, mdifferentiableWithinAt_iff_target, differentiableWithinAtProp_self_target, coe_trans_symm, Circle.argPartialEquiv_apply, ApproximatesLinearOn.to_inv, contMDiffWithinAt_iff_of_mem_source, IsMIntegralCurveAt.eventually_hasDerivAt, nhdsWithin_extChartAt_target_eq', Topology.RelCWComplex.map_zero_mem_closedCell, ModelWithCorners.toHomeomorph_symm_apply, ModelWithCorners.toPartialEquiv_coe_symm, SmoothBumpFunction.image_eq_inter_preimage_of_subset_support, SmoothBumpFunction.closedBall_subset, tangentBundleCore_coordChange_achart, pi_symm_apply, SmoothBumpFunction.isCompact_symm_image_closedBall, SmoothBumpFunction.ball_inter_range_eq_ball_inter_target
|
trans 📖 | CompOp | 51 mathmath: trans_target'', pi_trans, trans_source, ChartedSpaceCore.continuousOn_toFun, trans_apply, Equiv.trans_toPartialEquiv, trans_target', symm_trans_self, trans_source'', image_trans_source, OpenPartialHomeomorph.contDiffOn_extend_coord_change, trans_refl_restr, trans_source', trans_refl_restr', mem_symm_trans_source, OpenPartialHomeomorph.extend_coord_change_source_mem_nhdsWithin', Equiv.transPartialEquiv_trans, prod_trans, ext_coord_change_source, OpenPartialHomeomorph.trans_toPartialEquiv, OpenPartialHomeomorph.extend_image_source_inter, FiberBundle.extChartAt, trans_transEquiv, Pretrivialization.symm_trans_target_eq, contDiffOn_fderiv_coord_change, Trivialization.symm_trans_target_eq, transEquiv_eq_trans, contDiffOn_ext_coord_change, Pretrivialization.trans_source, coe_trans, trans_refl, trans_symm_eq_symm_trans_symm, ChartedSpaceCore.open_source, Trivialization.symm_trans_source_eq, trans_ofSet, inv_image_trans_target, EqOnSource.trans', Equidecomp.trans_toPartialEquiv, extChartAt_comp, Pretrivialization.symm_trans_symm, trans_target, restr_trans, TangentBundle.chartAt_toPartialEquiv, refl_trans, self_trans_symm, trans_assoc, OpenPartialHomeomorph.extend_coord_change_source, Pretrivialization.symm_trans_source_eq, coe_trans_symm, FiberBundleCore.localTrivAsPartialEquiv_trans, Equiv.transPartialEquiv_eq_trans
|
trans' 📖 | CompOp | 5 mathmath: OpenPartialHomeomorph.trans'_toPartialEquiv, trans'_target, trans'_apply, trans'_symm_apply, trans'_source
|
transEquiv 📖 | CompOp | 7 mathmath: transEquiv_symm_apply, transEquiv_transEquiv, transEquiv_target, trans_transEquiv, transEquiv_eq_trans, transEquiv_apply, transEquiv_source
|