Trivialization

📁 Source: Mathlib/Topology/FiberBundle/Trivialization.lean

Statistics

Metric	Count
Definitions Pretrivialization, baseSet, codExtend, codExtend', domExtend, instCoeFunForallProd, restrictPreimage, restrictPreimage', setSymm, toFun', toPartialEquiv, Trivialization, apply, symm_apply, baseSet, clift, codExtend, codExtend', compHomeomorph, coordChange, coordChangeHomeomorph, disjointUnion, domExtend, homeomorphComp, instCoeFunForallProd, instCoePretrivialization, liftCM, piecewise, piecewiseLe, piecewiseLeOfEq, preimageHomeomorph, aux, preimageSingletonHomeomorph, restrOpen, restrictPreimage, restrictPreimage', sourceHomeomorphBaseSetProd, aux, toFun', toOpenPartialHomeomorph, toPretrivialization, transFiberHomeomorph	42
Theorems apply_mk_symm, apply_symm_apply, apply_symm_apply', codExtend'_baseSet, codExtend'_source, codExtend'_target, codExtend'_toFun, codExtend_baseSet, codExtend_source, codExtend_target, codExtend_toFun, coe_coe, coe_coe_fst, coe_fst, coe_fst', coe_mem_source, coe_symm_of_notMem, domExtend_baseSet, domExtend_invFun, domExtend_source, domExtend_target, eqOn, ext, ext', ext'_iff, mem_source, mem_target, mk_mem_target, mk_proj_snd, mk_proj_snd', mk_symm, open_baseSet, open_target, preimage_symm_proj_baseSet, preimage_symm_proj_inter, proj_surjOn_baseSet, proj_symm_apply, proj_symm_apply', proj_toFun, restrictPreimage'_baseSet, restrictPreimage'_source, restrictPreimage'_target, restrictPreimage'_toFun, restrictPreimage_baseSet, restrictPreimage_source, restrictPreimage_target, restrictPreimage_toFun, source_eq, symm_apply, symm_apply_apply, symm_apply_apply_mk, symm_apply_mk_proj, symm_apply_of_notMem, symm_coe_proj, symm_proj_apply, symm_trans_source_eq, symm_trans_symm, symm_trans_target_eq, target_eq, target_inter_preimage_symm_source_eq, toPartialEquiv_injective, trans_source, apply_mk_symm, apply_symm_apply, apply_symm_apply', clift_self, codExtend'_apply, codExtend'_baseSet, codExtend'_source, codExtend'_target, codExtend_apply, codExtend_baseSet, codExtend_source, codExtend_target, coe_coe, coe_coe_fst, coe_fst, coe_fst', coe_fst_eventuallyEq_proj, coe_fst_eventuallyEq_proj', coe_mem_source, coe_mk, continuousAt_of_comp_left, continuousAt_of_comp_right, continuousAt_proj, continuousOn, continuousOn_proj, continuousOn_symm, continuous_coordChange, coordChangeHomeomorph_coe, coordChange_apply_snd, coordChange_coordChange, coordChange_same, coordChange_same_apply, domExtend_baseSet, domExtend_source, domExtend_symm_apply, domExtend_target, eqOn, ext', ext'_iff, frontier_preimage, image_preimage_eq_prod_univ, isImage_preimage_prod, lift_self, map_proj_nhds, map_target, mem_source, mem_target, mk_coordChange, mk_mem_target, mk_proj_snd, mk_proj_snd', mk_symm, nhds_eq_inf_comap, open_baseSet, preimageHomeomorph_apply, preimageHomeomorph_symm_apply, preimageSingletonHomeomorph_apply, preimageSingletonHomeomorph_symm_apply, preimage_subset_source, proj_clift, proj_lift, proj_surjOn_baseSet, proj_symm_apply, proj_symm_apply', proj_toFun, restrictPreimage'_apply, restrictPreimage'_baseSet, restrictPreimage'_source, restrictPreimage'_target, restrictPreimage_apply, restrictPreimage_baseSet, restrictPreimage_source, restrictPreimage_target, sourceHomeomorphBaseSetProd_apply, sourceHomeomorphBaseSetProd_symm_apply, source_eq, source_inter_preimage_target_inter, symm_apply, symm_apply_apply, symm_apply_apply_mk, symm_apply_mk_proj, symm_apply_of_notMem, symm_coe_proj, symm_proj_apply, symm_trans_source_eq, symm_trans_target_eq, target_eq, tendsto_nhds_iff, toPretrivialization_injective, transFiberHomeomorph_apply	152
Total	194

Bundle

Definitions

Name	Category	Theorems
Pretrivialization 📖	CompData	4 math math: Pretrivialization.toPartialEquiv_injective, Trivialization.toPretrivialization_injective, VectorPrebundle.pretrivialization_mem_atlas, FiberPrebundle.pretrivialization_mem_atlas
Trivialization 📖	CompData	9 math math: FiberBundle.trivialization_mem_atlas', MemTrivializationAtlas.out, Trivial.fiberBundle_trivializationAtlas', FiberBundle.pullback_trivializationAtlas', memTrivializationAtlas_iff, Trivialization.toPretrivialization_injective, FiberBundle.prod_trivializationAtlas', FiberBundle.trivialization_mem_atlas, FiberBundle.exists_trivialization_Icc_subset

Bundle.Pretrivialization

Definitions

Name	Category	Theorems
baseSet 📖	CompOp	33 math math: preimage_symm_proj_inter, mem_source, symm_trans_source_eq, trans_source, mem_target, ext'_iff, target_eq, symm_trans_target_eq, Bundle.Trivialization.codExtend_baseSet, codExtend'_baseSet, preimage_symm_proj_baseSet, Bundle.Trivialization.domExtend_baseSet, Bundle.Trivialization.restrictPreimage'_baseSet, source_eq, target_inter_preimage_symm_source_eq, open_baseSet, VectorPrebundle.exists_coordChange, restrictPreimage'_baseSet, restrictPreimage_baseSet, VectorPrebundle.mem_base_pretrivializationAt, codExtend_baseSet, Bundle.Trivialization.codExtend'_baseSet, VectorPrebundle.continuousOn_coordChange, VectorPrebundle.contMDiffOn_contMDiffCoordChange, domExtend_baseSet, mk_mem_target, coe_mem_source, VectorPrebundle.IsContMDiff.exists_contMDiffCoordChange, Bundle.Trivialization.restrictPreimage_baseSet, proj_surjOn_baseSet, coe_linearMapAt, FiberPrebundle.mem_base_pretrivializationAt, linearMapAt_apply
codExtend 📖	CompOp	4 math math: codExtend_toFun, codExtend_source, codExtend_baseSet, codExtend_target
codExtend' 📖	CompOp	4 math math: codExtend'_toFun, codExtend'_baseSet, codExtend'_source, codExtend'_target
domExtend 📖	CompOp	4 math math: domExtend_invFun, domExtend_baseSet, domExtend_source, domExtend_target
instCoeFunForallProd 📖	CompOp	—
restrictPreimage 📖	CompOp	4 math math: restrictPreimage_toFun, restrictPreimage_target, restrictPreimage_baseSet, restrictPreimage_source
restrictPreimage' 📖	CompOp	4 math math: restrictPreimage'_source, restrictPreimage'_toFun, restrictPreimage'_baseSet, restrictPreimage'_target
setSymm 📖	CompOp	—
toFun' 📖	CompOp	39 math math: symm_proj_apply, restrictPreimage_toFun, codExtend'_toFun, coe_coe, Bundle.Trivialization.restrictPreimage_apply, IsLinear.linear, symm_apply_apply, FiberPrebundle.continuous_trivChange, continuousLinearMap_apply, VectorPrebundle.mk_contMDiffCoordChange, codExtend_toFun, FiberPrebundle.totalSpaceMk_isInducing, apply_mk_symm, restrictPreimage'_toFun, coe_linearMapAt_of_mem, Bundle.Trivialization.restrictPreimage'_apply, mk_proj_snd', coe_coe_fst, VectorPrebundle.exists_coordChange, Bundle.Trivialization.codExtend_apply, VectorPrebundle.totalSpaceMk_isInducing, eqOn, VectorPrebundle.mk_coordChange, symm_apply_mk_proj, apply_symm_apply', apply_symm_apply, linearEquivAt_apply, coe_fst', VectorPrebundle.IsContMDiff.exists_contMDiffCoordChange, symm_apply_apply_mk, VectorPrebundle.coordChange_apply, coe_linearMapAt, mk_proj_snd, continuousLinearMapCoordChange_apply, VectorPrebundle.contMDiffCoordChange_apply, linearMapAt_apply, linear, Bundle.Trivialization.codExtend'_apply, coe_fst
toPartialEquiv 📖	CompOp	64 math math: restrictPreimage_toFun, FiberPrebundle.mem_pretrivializationAt_source, codExtend'_toFun, preimage_symm_proj_inter, mem_source, Bundle.Trivialization.codExtend_source, coe_coe, symm_trans_source_eq, Bundle.Trivialization.domExtend_target, trans_source, symm_apply_apply, FiberPrebundle.continuous_trivChange, mem_target, FiberPrebundle.continuous_symm_of_mem_pretrivializationAtlas, restrictPreimage'_source, ext'_iff, codExtend_toFun, restrictPreimage_target, toPartialEquiv_injective, target_eq, symm_trans_target_eq, restrictPreimage'_toFun, proj_symm_apply, preimage_symm_proj_baseSet, continuousLinearMap_symm_apply, FiberPrebundle.isOpen_target_of_mem_pretrivializationAtlas_inter, open_target, Bundle.Trivialization.restrictPreimage'_source, Bundle.Trivialization.codExtend_target, Bundle.Trivialization.restrictPreimage'_target, symm_coe_proj, source_eq, target_inter_preimage_symm_source_eq, domExtend_invFun, FiberPrebundle.isOpen_source, VectorPrebundle.mem_trivialization_at_source, codExtend_source, eqOn, Bundle.Trivialization.domExtend_symm_apply, Bundle.Trivialization.domExtend_source, symm_apply_mk_proj, codExtend'_source, restrictPreimage'_target, apply_symm_apply', apply_symm_apply, codExtend_target, Bundle.Trivialization.codExtend'_target, Bundle.Trivialization.restrictPreimage_target, symm_apply, mk_mem_target, VectorPrebundle.totalSpaceMk_preimage_source, coe_mem_source, symm_trans_symm, proj_toFun, Bundle.Trivialization.restrictPreimage_source, proj_symm_apply', domExtend_source, domExtend_target, codExtend'_target, proj_surjOn_baseSet, FiberPrebundle.totalSpaceMk_preimage_source, Bundle.Trivialization.codExtend'_source, mk_symm, restrictPreimage_source

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_mk_symm 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	toFun' Bundle.TotalSpace Bundle.TotalSpace.proj symm	—	mk_symm apply_symm_apply mk_mem_target
apply_symm_apply 📖	mathematical	Set Set.instMembership PartialEquiv.target toPartialEquiv	toFun' PartialEquiv.toFun PartialEquiv.symm toPartialEquiv	—	PartialEquiv.right_inv
apply_symm_apply' 📖	mathematical	Set Set.instMembership baseSet	toFun' PartialEquiv.toFun PartialEquiv.symm toPartialEquiv	—	apply_symm_apply mem_target
codExtend'_baseSet 📖	mathematical	IsOpen	baseSet Set Set.instMembership codExtend' Set.image Set.Elem instTopologicalSpaceSubtype	—	—
codExtend'_source 📖	mathematical	IsOpen	PartialEquiv.source toPartialEquiv Set Set.instMembership codExtend' Set.Elem instTopologicalSpaceSubtype	—	—
codExtend'_target 📖	mathematical	IsOpen	PartialEquiv.target toPartialEquiv Set Set.instMembership codExtend' Set.image Set.Elem instTopologicalSpaceSubtype	—	—
codExtend'_toFun 📖	mathematical	IsOpen	PartialEquiv.toFun toPartialEquiv Set Set.instMembership codExtend' Set.Elem toFun' instTopologicalSpaceSubtype	—	—
codExtend_baseSet 📖	mathematical	IsOpen Set.Nonempty	baseSet Set Set.instMembership codExtend Set.image Set.Elem instTopologicalSpaceSubtype	—	—
codExtend_source 📖	mathematical	IsOpen Set.Nonempty	PartialEquiv.source toPartialEquiv Set Set.instMembership codExtend Set.Elem instTopologicalSpaceSubtype	—	—
codExtend_target 📖	mathematical	IsOpen Set.Nonempty	PartialEquiv.target toPartialEquiv Set Set.instMembership codExtend Set.image Set.Elem instTopologicalSpaceSubtype	—	—
codExtend_toFun 📖	mathematical	IsOpen Set.Nonempty	PartialEquiv.toFun toPartialEquiv Set Set.instMembership codExtend Set.Elem toFun' instTopologicalSpaceSubtype	—	—
coe_coe 📖	mathematical	—	PartialEquiv.toFun toPartialEquiv toFun'	—	—
coe_coe_fst 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	toFun' Bundle.TotalSpace Bundle.TotalSpace.proj	—	coe_fst
coe_fst 📖	mathematical	Set Set.instMembership PartialEquiv.source toPartialEquiv	toFun'	—	proj_toFun
coe_fst' 📖	mathematical	Set Set.instMembership baseSet	toFun'	—	coe_fst mem_source
coe_mem_source 📖	mathematical	—	Bundle.TotalSpace Set Set.instMembership PartialEquiv.source toPartialEquiv Bundle.TotalSpace.proj baseSet	—	mem_source
coe_symm_of_notMem 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	symm Pi.instZero	—	—
domExtend_baseSet 📖	mathematical	—	baseSet domExtend Set.Elem Set.preimage Set Set.instMembership	—	—
domExtend_invFun 📖	mathematical	—	PartialEquiv.invFun toPartialEquiv domExtend Set Set.instMembership Set.preimage Set.Elem	—	—
domExtend_source 📖	mathematical	—	PartialEquiv.source toPartialEquiv domExtend Set.image Set Set.instMembership Set.preimage Set.Elem	—	—
domExtend_target 📖	mathematical	—	PartialEquiv.target toPartialEquiv domExtend Set.Elem Set.preimage Set Set.instMembership	—	—
eqOn 📖	mathematical	—	Set.EqOn toFun' PartialEquiv.source toPartialEquiv	—	coe_fst
ext 📖	—	toFun' PartialEquiv.toFun PartialEquiv.symm toPartialEquiv baseSet	—	—	ext' PartialEquiv.ext source_eq
ext' 📖	—	toPartialEquiv baseSet	—	—	—
ext'_iff 📖	mathematical	—	toPartialEquiv baseSet	—	ext'
mem_source 📖	mathematical	—	Set Set.instMembership PartialEquiv.source toPartialEquiv baseSet	—	source_eq Set.mem_preimage
mem_target 📖	mathematical	—	Set Set.instMembership PartialEquiv.target toPartialEquiv baseSet	—	target_eq Set.prod_univ Set.mem_preimage
mk_mem_target 📖	mathematical	—	Set Set.instMembership PartialEquiv.target Bundle.TotalSpace toPartialEquiv Bundle.TotalSpace.proj baseSet	—	mem_target
mk_proj_snd 📖	mathematical	Set Set.instMembership PartialEquiv.source toPartialEquiv	toFun'	—	coe_fst
mk_proj_snd' 📖	mathematical	Set Set.instMembership baseSet	toFun'	—	coe_fst'
mk_symm 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	symm PartialEquiv.toFun Bundle.TotalSpace PartialEquiv.symm toPartialEquiv Bundle.TotalSpace.proj	—	symm_coe_proj symm_apply Bundle.TotalSpace.mk_cast proj_symm_apply'
open_baseSet 📖	mathematical	—	IsOpen baseSet	—	—
open_target 📖	mathematical	—	IsOpen instTopologicalSpaceProd PartialEquiv.target toPartialEquiv	—	—
preimage_symm_proj_baseSet 📖	mathematical	—	Set Set.instInter Set.preimage PartialEquiv.toFun PartialEquiv.symm toPartialEquiv baseSet PartialEquiv.target	—	Set.inter_eq_right proj_symm_apply mem_target
preimage_symm_proj_inter 📖	mathematical	—	Set Set.instInter Set.preimage PartialEquiv.toFun PartialEquiv.symm toPartialEquiv SProd.sprod Set.instSProd baseSet Set.univ	—	Set.ext proj_symm_apply'
proj_surjOn_baseSet 📖	mathematical	—	Set.SurjOn PartialEquiv.source toPartialEquiv baseSet	—	PartialEquiv.map_target mem_target proj_symm_apply'
proj_symm_apply 📖	mathematical	Set Set.instMembership PartialEquiv.target toPartialEquiv	PartialEquiv.toFun PartialEquiv.symm toPartialEquiv	—	coe_fst PartialEquiv.map_target PartialEquiv.right_inv coe_coe
proj_symm_apply' 📖	mathematical	Set Set.instMembership baseSet	PartialEquiv.toFun PartialEquiv.symm toPartialEquiv	—	proj_symm_apply mem_target
proj_toFun 📖	mathematical	Set Set.instMembership PartialEquiv.source toPartialEquiv	PartialEquiv.toFun toPartialEquiv	—	—
restrictPreimage'_baseSet 📖	mathematical	—	baseSet Set.Elem Set.preimage instTopologicalSpaceSubtype Set Set.instMembership Set.restrictPreimage restrictPreimage'	—	—
restrictPreimage'_source 📖	mathematical	—	PartialEquiv.source Set.Elem Set.preimage toPartialEquiv instTopologicalSpaceSubtype Set Set.instMembership Set.restrictPreimage restrictPreimage'	—	—
restrictPreimage'_target 📖	mathematical	—	PartialEquiv.target Set.Elem Set.preimage toPartialEquiv instTopologicalSpaceSubtype Set Set.instMembership Set.restrictPreimage restrictPreimage'	—	—
restrictPreimage'_toFun 📖	mathematical	—	PartialEquiv.toFun Set.Elem Set.preimage toPartialEquiv instTopologicalSpaceSubtype Set Set.instMembership Set.restrictPreimage restrictPreimage' toFun'	—	—
restrictPreimage_baseSet 📖	mathematical	Set.Nonempty Set Set.instInter baseSet	baseSet Set.Elem Set.preimage instTopologicalSpaceSubtype Set Set.instMembership Set.restrictPreimage restrictPreimage	—	—
restrictPreimage_source 📖	mathematical	Set.Nonempty Set Set.instInter baseSet	PartialEquiv.source Set.Elem Set.preimage toPartialEquiv instTopologicalSpaceSubtype Set Set.instMembership Set.restrictPreimage restrictPreimage	—	—
restrictPreimage_target 📖	mathematical	Set.Nonempty Set Set.instInter baseSet	PartialEquiv.target Set.Elem Set.preimage toPartialEquiv instTopologicalSpaceSubtype Set Set.instMembership Set.restrictPreimage restrictPreimage	—	—
restrictPreimage_toFun 📖	mathematical	Set.Nonempty Set Set.instInter baseSet	PartialEquiv.toFun Set.Elem Set.preimage toPartialEquiv instTopologicalSpaceSubtype Set Set.instMembership Set.restrictPreimage restrictPreimage toFun'	—	—
source_eq 📖	mathematical	—	PartialEquiv.source toPartialEquiv Set.preimage baseSet	—	—
symm_apply 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	symm Bundle.TotalSpace.proj PartialEquiv.toFun Bundle.TotalSpace PartialEquiv.symm toPartialEquiv symm_coe_proj Bundle.TotalSpace.snd	—	—
symm_apply_apply 📖	mathematical	Set Set.instMembership PartialEquiv.source toPartialEquiv	PartialEquiv.toFun PartialEquiv.symm toPartialEquiv toFun'	—	PartialEquiv.left_inv
symm_apply_apply_mk 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	symm toFun' Bundle.TotalSpace Bundle.TotalSpace.proj	—	symm_proj_apply
symm_apply_mk_proj 📖	mathematical	Set Set.instMembership PartialEquiv.source toPartialEquiv	PartialEquiv.toFun PartialEquiv.symm toPartialEquiv toFun'	—	coe_fst coe_coe PartialEquiv.left_inv
symm_apply_of_notMem 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	symm	—	—
symm_coe_proj 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	Bundle.TotalSpace.proj PartialEquiv.toFun Bundle.TotalSpace PartialEquiv.symm toPartialEquiv	—	proj_symm_apply'
symm_proj_apply 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	symm Bundle.TotalSpace.proj toFun' Bundle.TotalSpace Bundle.TotalSpace.snd	—	symm_coe_proj symm_apply mk_proj_snd' symm_apply_apply mem_source
symm_trans_source_eq 📖	mathematical	—	PartialEquiv.source PartialEquiv.trans PartialEquiv.symm toPartialEquiv SProd.sprod Set Set.instSProd Set.instInter baseSet Set.univ	—	PartialEquiv.trans_source source_eq PartialEquiv.symm_source target_eq Set.inter_comm preimage_symm_proj_inter
symm_trans_symm 📖	mathematical	—	PartialEquiv.symm PartialEquiv.trans toPartialEquiv	—	PartialEquiv.trans_symm_eq_symm_trans_symm PartialEquiv.symm_symm
symm_trans_target_eq 📖	mathematical	—	PartialEquiv.target PartialEquiv.trans PartialEquiv.symm toPartialEquiv SProd.sprod Set Set.instSProd Set.instInter baseSet Set.univ	—	PartialEquiv.symm_source symm_trans_symm symm_trans_source_eq Set.inter_comm
target_eq 📖	mathematical	—	PartialEquiv.target toPartialEquiv SProd.sprod Set Set.instSProd baseSet Set.univ	—	—
target_inter_preimage_symm_source_eq 📖	mathematical	—	Set Set.instInter PartialEquiv.target toPartialEquiv Set.preimage PartialEquiv.toFun PartialEquiv.symm PartialEquiv.source SProd.sprod Set.instSProd baseSet Set.univ	—	Set.inter_comm target_eq source_eq preimage_symm_proj_inter
toPartialEquiv_injective 📖	mathematical	—	Bundle.Pretrivialization PartialEquiv toPartialEquiv	—	ext' target_eq Set.fst_image_prod
trans_source 📖	mathematical	—	PartialEquiv.source PartialEquiv.trans PartialEquiv.symm toPartialEquiv SProd.sprod Set Set.instSProd Set.instInter baseSet Set.univ	—	PartialEquiv.trans_source PartialEquiv.symm_source target_inter_preimage_symm_source_eq

Bundle.Trivialization

Definitions

Name	Category	Theorems
baseSet 📖	CompOp	78 math math: contMDiffOn_section_baseSet_iff, FiberBundle.mem_baseSet_trivializationAt', mdifferentiableOn_symm_coordChangeL, VectorBundleCore.mem_localTriv_target, source_eq, Prod.continuous_inv_fun, contMDiffOn_baseSet_iff_localFrame_coeff, proj_clift, FiberBundleCore.mem_localTrivAt_source, continuousLinearEquivAt_apply', comp_continuousLinearEquivAt_eq_coord_change, prod_baseSet, continuousLinearEquivAt_prod, open_baseSet, prod_source, mdifferentiableOn_section_baseSet_iff, contMDiffOn_localFrame_baseSet, FiberBundleCore.baseSet_at, VectorBundleCore.baseSet_at, codExtend_baseSet, prod_target, contMDiffOn_baseSet_localFrame_coeff, continuousOn_symm, FiberBundleCore.mem_localTriv_source, Bundle.Pretrivialization.continuousOn_continuousLinearMapCoordChange, target_eq, coe_coordChangeL, contMDiffOn_continuousLinearMapCoordChange, VectorBundle.continuousOn_coordChange', pullback_baseSet, FiberBundleCore.mem_localTrivAt_target, domExtend_baseSet, Topology.IsQuotientMap.trivializationOfSMulDisjoint_baseSet, IsOpen.trivializationDiscrete_baseSet, contMDiffOn_symm_coordChangeL, FiberBundleCore.mem_localTriv_target, restrictPreimage'_baseSet, mdifferentiableOn_baseSet_localFrame_coeff, symm_trans_target_eq, ext'_iff, isLocalFrameOn_localFrame_baseSet, baseSet_continuousLinearMap, mdifferentiableOn_continuousLinearMapCoordChange, mk_mem_target, linearMapAt_apply, mem_source, hom_trivializationAt_source, mdifferentiableOn_coordChangeL, FiberBundle.extChartAt_target, coordChangeL_symm_apply, ContMDiffVectorBundle.contMDiffOn_coordChangeL, clift_self, tangentBundleCore_localTriv_baseSet, Prod.continuous_to_fun, codExtend'_baseSet, FiberBundle.exists_trivialization_Icc_subset, TangentBundle.trivializationAt_baseSet, frontier_preimage, Topology.IsQuotientMap.trivializationOfVAddDisjoint_baseSet, sourceHomeomorphBaseSetProd_apply, FiberBundleCore.mem_localTrivAt_baseSet, contMDiffOn_coordChangeL, proj_surjOn_baseSet, hom_trivializationAt_baseSet, IsEvenlyCovered.mem_toTrivialization_baseSet, VectorBundleCore.mem_localTrivAt_baseSet, FiberBundle.mem_baseSet_trivializationAt, Bundle.Trivial.trivialization_baseSet, sourceHomeomorphBaseSetProd_symm_apply, mem_target, coe_linearMapAt, restrictPreimage_baseSet, symm_trans_source_eq, hom_trivializationAt_target, coe_coordChangeL', pullback_target, continuousOn_coordChange, coe_mem_source
clift 📖	CompOp	2 math math: proj_clift, clift_self
codExtend 📖	CompOp	4 math math: codExtend_source, codExtend_baseSet, codExtend_target, codExtend_apply
codExtend' 📖	CompOp	4 math math: codExtend'_baseSet, codExtend'_target, codExtend'_source, codExtend'_apply
compHomeomorph 📖	CompOp	—
coordChange 📖	CompOp	15 math math: continuous_coordChange, ContMDiffWithinAt.coordChange, ContMDiff.coordChange, MDifferentiableWithinAt.coordChange, coordChange_apply_snd, MDifferentiable.coordChange, MDifferentiableAt.coordChange, coordChange_same_apply, coordChange_same, coordChange_coordChange, MDifferentiableOn.coordChange, mk_coordChange, ContMDiffOn.coordChange, ContMDiffAt.coordChange, coordChangeHomeomorph_coe
coordChangeHomeomorph 📖	CompOp	1 math math: coordChangeHomeomorph_coe
disjointUnion 📖	CompOp	—
domExtend 📖	CompOp	4 math math: domExtend_target, domExtend_baseSet, domExtend_symm_apply, domExtend_source
homeomorphComp 📖	CompOp	—
instCoeFunForallProd 📖	CompOp	—
instCoePretrivialization 📖	CompOp	—
liftCM 📖	CompOp	—
piecewise 📖	CompOp	—
piecewiseLe 📖	CompOp	—
piecewiseLeOfEq 📖	CompOp	—
preimageHomeomorph 📖	CompOp	2 math math: preimageHomeomorph_apply, preimageHomeomorph_symm_apply
preimageSingletonHomeomorph 📖	CompOp	2 math math: preimageSingletonHomeomorph_apply, preimageSingletonHomeomorph_symm_apply
restrOpen 📖	CompOp	—
restrictPreimage 📖	CompOp	4 math math: restrictPreimage_apply, restrictPreimage_target, restrictPreimage_source, restrictPreimage_baseSet
restrictPreimage' 📖	CompOp	4 math math: restrictPreimage'_apply, restrictPreimage'_source, restrictPreimage'_baseSet, restrictPreimage'_target
sourceHomeomorphBaseSetProd 📖	CompOp	2 math math: sourceHomeomorphBaseSetProd_apply, sourceHomeomorphBaseSetProd_symm_apply
toFun' 📖	CompOp	99 math math: mdifferentiableWithinAt_totalSpace, contMDiffOn_section_baseSet_iff, restrictPreimage_apply, coordChangeL_apply, image_preimage_eq_prod_univ, contMDiffOn, coe_fst, FiberBundle.continuousAt_totalSpace, symm_proj_apply, mdifferentiableWithinAt_section, FiberBundle.continuousWithinAt_totalSpace, localFrame_coeff_eq_coeff, coe_fst', apply_symm_apply, VectorBundleCore.localTrivAt_apply, TangentBundle.trivializationAt_fst, eqOn, mdifferentiableAt_section_iff, continuousLinearEquivAt_apply', mdifferentiableAt_totalSpace, coordChange_apply_snd, symm_apply_apply, IsLinear.linear, FiberBundleCore.localTrivAsPartialEquiv_coe, preimageHomeomorph_apply, preimageSingletonHomeomorph_apply, prod_apply', TangentBundle.trivializationAt_apply, ContMDiffWithinAt.change_section_trivialization, mdifferentiableWithinAt_totalSpace_iff, mdifferentiableOn_section_baseSet_iff, apply_symm_apply_eq_coordChangeL, FiberBundle.writtenInExtChartAt_trivializationAt, coe_linearMapAt_of_mem, FiberBundleCore.localTriv_apply, FiberBundleCore.localTrivAt_apply, VectorBundle.continuousLinearEquivAt_apply, trivializationAt_model_space_apply, IsEvenlyCovered.toTrivialization_apply, mdifferentiableOn_section_iff, Bundle.Trivial.trivialization_apply, Bundle.contMDiffWithinAt_totalSpace, restrictPreimage'_apply, contMDiffWithinAt_iff, FiberBundle.trivializationAt_proj_fst, zeroSection, linearEquivAt_apply, VectorBundleCore.localTriv_apply, Bundle.contMDiffAt_totalSpace, linear, mk_proj_snd', tendsto_nhds_iff, continuousLinearEquivAt_apply, codExtend_apply, linearMapAt_apply, apply_eq_prod_continuousLinearEquivAt, contMDiff_iff, coe_coe, continuousLinearMap_apply, VectorBundleCore.localTrivAt_apply_mk, mdifferentiableAt_section, contMDiffAt_section_iff, FiberBundle.writtenInExtChartAt_trivializationAt_symm, coe_fst_eventuallyEq_proj', coe_coe_fst, nhds_eq_inf_comap, contMDiffAt_iff, Bundle.contMDiffAt_section, contMDiffWithinAt_section, continuousOn, source_inter_preimage_target_inter, symm_apply_mk_proj, mk_coordChange, sourceHomeomorphBaseSetProd_apply, mk_coordChangeL, coordChangeL_apply', apply_symm_apply', hom_trivializationAt_apply, Bundle.contMDiffWithinAt_section, symm_apply_apply_mk, mdifferentiableAt_snd_comp_iff₂, contMDiffOn_iff, mdifferentiableWithinAt_section_iff, contMDiffWithinAt_snd_comp_iff₂, coe_linearMapAt, coe_mk, contMDiffOn_section_iff, coe_fst_eventuallyEq_proj, prod_apply, mdifferentiableWithinAt_snd_comp_iff₂, MDifferentiableWithinAt.change_section_trivialization, pullback_apply, apply_mk_symm, mk_proj_snd, FiberBundleCore.localTrivAt_apply_mk, mdifferentiableAt_totalSpace_iff, transFiberHomeomorph_apply, codExtend'_apply, FiberBundleCore.localTrivAt_snd
toOpenPartialHomeomorph 📖	CompOp	98 math math: pullback_symm_apply_proj, IsOpen.trivializationDiscrete_target, codExtend_source, domExtend_target, symm_apply_eq_mk_continuousLinearEquivAt_symm, contMDiffOn, VectorBundleCore.mem_localTriv_target, source_eq, FiberBundleCore.mk_mem_localTrivAt_source, proj_clift, FiberBundleCore.mem_localTrivAt_source, prod_symm_apply_proj, symm_apply, isImage_preimage_prod, prod_symm_apply, VectorBundleCore.localTriv_symm_fst, FiberBundleCore.localTrivAsPartialEquiv_target, apply_symm_apply, mk_symm, eqOn, continuousLinearEquivAt_apply', Bundle.Trivial.trivialization_target, FiberBundle.chartedSpace_chartAt, symm_apply_apply, prod_symm_apply_snd, preimageHomeomorph_symm_apply, prod_source, apply_symm_apply_eq_coordChangeL, prod_target, FiberBundleCore.mem_localTriv_source, target_eq, VectorBundleCore.mem_source_at, FiberBundle.chartedSpace'_chartAt, FiberBundleCore.mem_localTrivAt_target, TangentBundle.trivializationAt_source, pullback_source, TangentBundle.chartAt, restrictPreimage'_source, preimageSingletonHomeomorph_symm_apply, FiberBundleCore.mem_localTriv_target, FiberBundle.extChartAt, codExtend_target, symm_trans_target_eq, restrictPreimage'_target, ext'_iff, symm_coe_proj, mk_mem_target, continuousOn_proj, Bundle.Trivial.toOpenPartialHomeomorph_trivialization_symm_apply, IsOpen.trivializationDiscrete_source, FiberBundleCore.localTrivAsPartialEquiv_source, mem_source, coe_coe, hom_trivializationAt_source, domExtend_symm_apply, domExtend_source, FiberBundle.mem_trivializationAt_proj_source, Topology.IsQuotientMap.trivializationOfVAddDisjoint_source, clift_self, FiberBundle.writtenInExtChartAt_trivializationAt_symm, proj_symm_apply, Topology.IsQuotientMap.trivializationOfSMulDisjoint_target, pullback_symm_apply_snd, continuousOn, source_inter_preimage_target_inter, symm_apply_mk_proj, contMDiffOn_symm, map_target, frontier_preimage, mk_coordChange, codExtend'_target, sourceHomeomorphBaseSetProd_apply, VectorBundleCore.mem_localTriv_source, restrictPreimage_target, preimage_subset_source, coordChangeL_apply', Topology.IsQuotientMap.trivializationOfSMulDisjoint_source, apply_symm_apply', proj_surjOn_baseSet, restrictPreimage_source, sourceHomeomorphBaseSetProd_symm_apply, Bundle.Trivial.trivialization_symm_apply_proj, Topology.IsQuotientMap.trivializationOfVAddDisjoint_target, mem_target, symm_trans_source_eq, proj_symm_apply', codExtend'_source, contMDiffOn_symm_trans, hom_trivializationAt_target, Bundle.Trivial.trivialization_source, pullback_target, Bundle.Trivial.trivialization_symm_apply_snd, FiberBundleCore.localTrivAsPartialEquiv_symm, coe_mem_source, FiberBundleCore.localTriv_symm_apply, Bundle.Trivialization.mdifferentiable, TangentBundle.trivializationAt_target, proj_toFun
toPretrivialization 📖	CompOp	22 math math: codExtend_source, restrictPreimage_apply, domExtend_target, codExtend_baseSet, toPretrivialization_injective, toPretrivialization.isLinear, restrictPreimage'_apply, domExtend_baseSet, restrictPreimage'_source, restrictPreimage'_baseSet, codExtend_target, restrictPreimage'_target, codExtend_apply, domExtend_symm_apply, domExtend_source, codExtend'_baseSet, codExtend'_target, restrictPreimage_target, restrictPreimage_source, restrictPreimage_baseSet, codExtend'_source, codExtend'_apply
transFiberHomeomorph 📖	CompOp	1 math math: transFiberHomeomorph_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_mk_symm 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	toFun' Bundle.TotalSpace Bundle.TotalSpace.proj symm	—	Bundle.Pretrivialization.apply_mk_symm
apply_symm_apply 📖	mathematical	Set Set.instMembership PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd toOpenPartialHomeomorph	toFun' OpenPartialHomeomorph.toFun' instTopologicalSpaceProd OpenPartialHomeomorph.symm toOpenPartialHomeomorph	—	OpenPartialHomeomorph.right_inv
apply_symm_apply' 📖	mathematical	Set Set.instMembership baseSet	toFun' OpenPartialHomeomorph.toFun' instTopologicalSpaceProd OpenPartialHomeomorph.symm toOpenPartialHomeomorph	—	Bundle.Pretrivialization.apply_symm_apply'
clift_self 📖	mathematical	Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd toOpenPartialHomeomorph baseSet DFunLike.coe ContinuousMap Set.Elem instTopologicalSpaceSubtype ContinuousMap.instFunLike	DFunLike.coe ContinuousMap Set.Elem PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd toOpenPartialHomeomorph instTopologicalSpaceSubtype Set Set.instMembership ContinuousMap.instFunLike baseSet ContinuousMap.compactOpen clift	—	lift_self Subtype.coe_eta
codExtend'_apply 📖	mathematical	IsOpen	toFun' Set Set.instMembership codExtend' Set.Elem Bundle.Pretrivialization.toFun' instTopologicalSpaceSubtype toPretrivialization	—	—
codExtend'_baseSet 📖	mathematical	IsOpen	baseSet Set Set.instMembership codExtend' Set.image Bundle.Pretrivialization.baseSet Set.Elem instTopologicalSpaceSubtype toPretrivialization	—	—
codExtend'_source 📖	mathematical	IsOpen	PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd toOpenPartialHomeomorph Set Set.instMembership codExtend' Set.Elem Bundle.Pretrivialization.toPartialEquiv instTopologicalSpaceSubtype toPretrivialization	—	—
codExtend'_target 📖	mathematical	IsOpen	PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd toOpenPartialHomeomorph Set Set.instMembership codExtend' Set.image Set.Elem Bundle.Pretrivialization.toPartialEquiv instTopologicalSpaceSubtype toPretrivialization	—	—
codExtend_apply 📖	mathematical	IsOpen Set.Nonempty	toFun' Set Set.instMembership codExtend Set.Elem Bundle.Pretrivialization.toFun' instTopologicalSpaceSubtype toPretrivialization	—	—
codExtend_baseSet 📖	mathematical	IsOpen Set.Nonempty	baseSet Set Set.instMembership codExtend Set.image Bundle.Pretrivialization.baseSet Set.Elem instTopologicalSpaceSubtype toPretrivialization	—	—
codExtend_source 📖	mathematical	IsOpen Set.Nonempty	PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd toOpenPartialHomeomorph Set Set.instMembership codExtend Set.Elem Bundle.Pretrivialization.toPartialEquiv instTopologicalSpaceSubtype toPretrivialization	—	—
codExtend_target 📖	mathematical	IsOpen Set.Nonempty	PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd toOpenPartialHomeomorph Set Set.instMembership codExtend Set.image Set.Elem Bundle.Pretrivialization.toPartialEquiv instTopologicalSpaceSubtype toPretrivialization	—	—
coe_coe 📖	mathematical	—	OpenPartialHomeomorph.toFun' instTopologicalSpaceProd toOpenPartialHomeomorph toFun'	—	—
coe_coe_fst 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	toFun' Bundle.TotalSpace Bundle.TotalSpace.proj	—	coe_fst mem_source
coe_fst 📖	mathematical	Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd toOpenPartialHomeomorph	toFun'	—	proj_toFun
coe_fst' 📖	mathematical	Set Set.instMembership baseSet	toFun'	—	coe_fst mem_source
coe_fst_eventuallyEq_proj 📖	mathematical	Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd toOpenPartialHomeomorph	Filter.EventuallyEq nhds toFun'	—	mem_nhds_iff coe_fst OpenPartialHomeomorph.open_source
coe_fst_eventuallyEq_proj' 📖	mathematical	Set Set.instMembership baseSet	Filter.EventuallyEq nhds toFun'	—	coe_fst_eventuallyEq_proj mem_source
coe_mem_source 📖	mathematical	—	Bundle.TotalSpace Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd toOpenPartialHomeomorph Bundle.TotalSpace.proj baseSet	—	mem_source
coe_mk 📖	mathematical	IsOpen PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd Set.preimage PartialEquiv.target SProd.sprod Set Set.instSProd Set.univ OpenPartialHomeomorph.toFun'	toFun' OpenPartialHomeomorph.toFun' instTopologicalSpaceProd	—	—
continuousAt_of_comp_left 📖	mathematical	ContinuousAt Set Set.instMembership baseSet instTopologicalSpaceProd toFun'	ContinuousAt	—	OpenPartialHomeomorph.continuousAt_iff_continuousAt_comp_left source_eq Set.preimage_comp ContinuousAt.preimage_mem_nhds IsOpen.mem_nhds open_baseSet
continuousAt_of_comp_right 📖	mathematical	Set Set.instMembership baseSet ContinuousAt instTopologicalSpaceProd PartialEquiv.toFun PartialEquiv.symm OpenPartialHomeomorph.toPartialEquiv toOpenPartialHomeomorph toFun'	ContinuousAt	—	PartialEquiv.symm_target mem_source OpenPartialHomeomorph.continuousAt_iff_continuousAt_comp_right OpenPartialHomeomorph.symm_symm
continuousAt_proj 📖	mathematical	Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd toOpenPartialHomeomorph	ContinuousAt	—	Eq.le map_proj_nhds
continuousOn 📖	mathematical	—	ContinuousOn Bundle.TotalSpace instTopologicalSpaceProd toFun' Bundle.TotalSpace.proj PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv toOpenPartialHomeomorph	—	OpenPartialHomeomorph.continuousOn_toFun
continuousOn_proj 📖	mathematical	—	ContinuousOn PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd toOpenPartialHomeomorph	—	continuousOn_of_forall_continuousAt continuousAt_proj
continuousOn_symm 📖	mathematical	—	ContinuousOn Bundle.TotalSpace instTopologicalSpaceProd Bundle.TotalSpace.mk' symm SProd.sprod Set Set.instSProd baseSet Bundle.TotalSpace.proj Set.univ	—	mk_symm ContinuousOn.congr target_eq OpenPartialHomeomorph.continuousOn_symm
continuous_coordChange 📖	mathematical	Set Set.instMembership baseSet	Continuous coordChange	—	Continuous.comp continuous_snd ContinuousOn.comp_continuous OpenPartialHomeomorph.continuousOn OpenPartialHomeomorph.continuousOn_symm Continuous.prodMk continuous_const continuous_id' mem_target mem_source proj_symm_apply'
coordChangeHomeomorph_coe 📖	mathematical	Set Set.instMembership baseSet	DFunLike.coe Homeomorph EquivLike.toFunLike Homeomorph.instEquivLike coordChangeHomeomorph coordChange	—	—
coordChange_apply_snd 📖	mathematical	Set Set.instMembership baseSet	coordChange toFun'	—	coordChange.eq_1 symm_apply_mk_proj mem_source
coordChange_coordChange 📖	mathematical	Set Set.instMembership baseSet	coordChange	—	coordChange.eq_1 mk_coordChange coe_coe OpenPartialHomeomorph.left_inv mem_source proj_symm_apply'
coordChange_same 📖	mathematical	Set Set.instMembership baseSet	coordChange	—	coordChange_same_apply
coordChange_same_apply 📖	mathematical	Set Set.instMembership baseSet	coordChange	—	coordChange.eq_1 apply_symm_apply'
domExtend_baseSet 📖	mathematical	IsOpen Set.preimage	baseSet domExtend Bundle.Pretrivialization.baseSet Set.Elem Set.preimage Set Set.instMembership toPretrivialization instTopologicalSpaceSubtype	—	—
domExtend_source 📖	mathematical	IsOpen Set.preimage	PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd toOpenPartialHomeomorph domExtend Set.image Set Set.instMembership Set.preimage Set.Elem Bundle.Pretrivialization.toPartialEquiv toPretrivialization instTopologicalSpaceSubtype	—	—
domExtend_symm_apply 📖	mathematical	IsOpen Set.preimage	OpenPartialHomeomorph.toFun' instTopologicalSpaceProd OpenPartialHomeomorph.symm toOpenPartialHomeomorph domExtend Set Set.instMembership Set.preimage PartialEquiv.toFun Set.Elem PartialEquiv.symm Bundle.Pretrivialization.toPartialEquiv toPretrivialization instTopologicalSpaceSubtype	—	—
domExtend_target 📖	mathematical	IsOpen Set.preimage	PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd toOpenPartialHomeomorph domExtend Set.Elem Set.preimage Bundle.Pretrivialization.toPartialEquiv Set Set.instMembership toPretrivialization instTopologicalSpaceSubtype	—	—
eqOn 📖	mathematical	—	Set.EqOn toFun' PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd toOpenPartialHomeomorph	—	coe_fst
ext' 📖	—	toOpenPartialHomeomorph baseSet	—	—	—
ext'_iff 📖	mathematical	—	toOpenPartialHomeomorph baseSet	—	ext'
frontier_preimage 📖	mathematical	—	Set Set.instInter PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd toOpenPartialHomeomorph frontier Set.preimage baseSet	—	OpenPartialHomeomorph.IsImage.preimage_eq OpenPartialHomeomorph.IsImage.frontier isImage_preimage_prod frontier_prod_univ_eq source_eq Set.preimage_inter
image_preimage_eq_prod_univ 📖	mathematical	Set Set.instHasSubset baseSet	Set.image toFun' Set.preimage SProd.sprod Set Set.instSProd Set.univ	—	Set.Subset.antisymm Set.image_subset_iff proj_toFun preimage_subset_source mem_target Set.mem_preimage proj_symm_apply apply_symm_apply
isImage_preimage_prod 📖	mathematical	—	OpenPartialHomeomorph.IsImage instTopologicalSpaceProd toOpenPartialHomeomorph Set.preimage SProd.sprod Set Set.instSProd Set.univ	—	coe_fst
lift_self 📖	mathematical	Set Set.instMembership baseSet	lift	—	symm_apply_mk_proj mem_source
map_proj_nhds 📖	mathematical	Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd toOpenPartialHomeomorph	Filter.map nhds	—	coe_fst Filter.map_congr coe_fst_eventuallyEq_proj Filter.map_map coe_coe OpenPartialHomeomorph.map_nhds_eq map_fst_nhds
map_target 📖	mathematical	Set Set.instMembership PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd toOpenPartialHomeomorph	Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd toOpenPartialHomeomorph OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm	—	OpenPartialHomeomorph.map_target
mem_source 📖	mathematical	—	Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd toOpenPartialHomeomorph baseSet	—	source_eq Set.mem_preimage
mem_target 📖	mathematical	—	Set Set.instMembership PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd toOpenPartialHomeomorph baseSet	—	Bundle.Pretrivialization.mem_target
mk_coordChange 📖	mathematical	Set Set.instMembership baseSet	coordChange toFun' OpenPartialHomeomorph.toFun' instTopologicalSpaceProd OpenPartialHomeomorph.symm toOpenPartialHomeomorph	—	coe_fst' proj_symm_apply' apply_symm_apply'
mk_mem_target 📖	mathematical	—	Set Set.instMembership PartialEquiv.target Bundle.TotalSpace OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd toOpenPartialHomeomorph Bundle.TotalSpace.proj baseSet	—	Bundle.Pretrivialization.mem_target
mk_proj_snd 📖	mathematical	Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd toOpenPartialHomeomorph	toFun'	—	coe_fst
mk_proj_snd' 📖	mathematical	Set Set.instMembership baseSet	toFun'	—	coe_fst'
mk_symm 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	symm OpenPartialHomeomorph.toFun' Bundle.TotalSpace instTopologicalSpaceProd OpenPartialHomeomorph.symm toOpenPartialHomeomorph Bundle.TotalSpace.proj	—	Bundle.Pretrivialization.mk_symm
nhds_eq_inf_comap 📖	mathematical	Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd toOpenPartialHomeomorph	nhds Filter Filter.instInf Filter.comap toFun'	—	eq_of_forall_le_iff le_inf_iff Filter.tendsto_iff_comap tendsto_nhds_iff
open_baseSet 📖	mathematical	—	IsOpen baseSet	—	—
preimageHomeomorph_apply 📖	mathematical	Set Set.instHasSubset baseSet	DFunLike.coe Homeomorph Set.Elem Set.preimage instTopologicalSpaceSubtype Set Set.instMembership instTopologicalSpaceProd EquivLike.toFunLike Homeomorph.instEquivLike preimageHomeomorph toFun'	—	proj_toFun mem_source
preimageHomeomorph_symm_apply 📖	mathematical	Set Set.instHasSubset baseSet	DFunLike.coe Homeomorph Set.Elem Set.preimage instTopologicalSpaceProd instTopologicalSpaceSubtype Set Set.instMembership EquivLike.toFunLike Homeomorph.instEquivLike Homeomorph.symm preimageHomeomorph OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm toOpenPartialHomeomorph preimageHomeomorph_symm_apply.aux	—	—
preimageSingletonHomeomorph_apply 📖	mathematical	Set Set.instMembership baseSet	DFunLike.coe Homeomorph Set.Elem Set.preimage Set Set.instSingletonSet instTopologicalSpaceSubtype Set.instMembership EquivLike.toFunLike Homeomorph.instEquivLike preimageSingletonHomeomorph toFun'	—	—
preimageSingletonHomeomorph_symm_apply 📖	mathematical	Set Set.instMembership baseSet	DFunLike.coe Homeomorph Set.Elem Set.preimage Set Set.instSingletonSet instTopologicalSpaceSubtype Set.instMembership EquivLike.toFunLike Homeomorph.instEquivLike Homeomorph.symm preimageSingletonHomeomorph OpenPartialHomeomorph.toFun' instTopologicalSpaceProd OpenPartialHomeomorph.symm toOpenPartialHomeomorph	—	—
preimage_subset_source 📖	mathematical	Set Set.instHasSubset baseSet	Set Set.instHasSubset Set.preimage PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd toOpenPartialHomeomorph	—	mem_source
proj_clift 📖	mathematical	—	Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd toOpenPartialHomeomorph DFunLike.coe ContinuousMap Set.Elem instTopologicalSpaceSubtype ContinuousMap.instFunLike baseSet ContinuousMap.compactOpen clift	—	proj_lift
proj_lift 📖	mathematical	Set Set.instMembership baseSet	lift	—	proj_symm_apply mem_target
proj_surjOn_baseSet 📖	mathematical	—	Set.SurjOn PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd toOpenPartialHomeomorph baseSet	—	Bundle.Pretrivialization.proj_surjOn_baseSet
proj_symm_apply 📖	mathematical	Set Set.instMembership PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd toOpenPartialHomeomorph	OpenPartialHomeomorph.toFun' instTopologicalSpaceProd OpenPartialHomeomorph.symm toOpenPartialHomeomorph	—	Bundle.Pretrivialization.proj_symm_apply
proj_symm_apply' 📖	mathematical	Set Set.instMembership baseSet	OpenPartialHomeomorph.toFun' instTopologicalSpaceProd OpenPartialHomeomorph.symm toOpenPartialHomeomorph	—	Bundle.Pretrivialization.proj_symm_apply'
proj_toFun 📖	mathematical	Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd toOpenPartialHomeomorph	OpenPartialHomeomorph.toFun' instTopologicalSpaceProd toOpenPartialHomeomorph	—	—
restrictPreimage'_apply 📖	mathematical	—	toFun' Set.Elem Set.preimage instTopologicalSpaceSubtype Set Set.instMembership Set.restrictPreimage restrictPreimage' Bundle.Pretrivialization.toFun' toPretrivialization	—	—
restrictPreimage'_baseSet 📖	mathematical	—	baseSet Set.Elem Set.preimage instTopologicalSpaceSubtype Set Set.instMembership Set.restrictPreimage restrictPreimage' Bundle.Pretrivialization.baseSet toPretrivialization	—	—
restrictPreimage'_source 📖	mathematical	—	PartialEquiv.source Set.Elem Set.preimage OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceSubtype Set Set.instMembership instTopologicalSpaceProd toOpenPartialHomeomorph Set.restrictPreimage restrictPreimage' Bundle.Pretrivialization.toPartialEquiv toPretrivialization	—	—
restrictPreimage'_target 📖	mathematical	—	PartialEquiv.target Set.Elem Set.preimage OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceSubtype Set Set.instMembership instTopologicalSpaceProd toOpenPartialHomeomorph Set.restrictPreimage restrictPreimage' Bundle.Pretrivialization.toPartialEquiv toPretrivialization	—	—
restrictPreimage_apply 📖	mathematical	Set.Nonempty Set Set.instInter baseSet	toFun' Set.Elem Set.preimage instTopologicalSpaceSubtype Set Set.instMembership Set.restrictPreimage restrictPreimage Bundle.Pretrivialization.toFun' toPretrivialization	—	—
restrictPreimage_baseSet 📖	mathematical	Set.Nonempty Set Set.instInter baseSet	baseSet Set.Elem Set.preimage instTopologicalSpaceSubtype Set Set.instMembership Set.restrictPreimage restrictPreimage Bundle.Pretrivialization.baseSet toPretrivialization	—	—
restrictPreimage_source 📖	mathematical	Set.Nonempty Set Set.instInter baseSet	PartialEquiv.source Set.Elem Set.preimage OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceSubtype Set Set.instMembership instTopologicalSpaceProd toOpenPartialHomeomorph Set.restrictPreimage restrictPreimage Bundle.Pretrivialization.toPartialEquiv toPretrivialization	—	—
restrictPreimage_target 📖	mathematical	Set.Nonempty Set Set.instInter baseSet	PartialEquiv.target Set.Elem Set.preimage OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceSubtype Set Set.instMembership instTopologicalSpaceProd toOpenPartialHomeomorph Set.restrictPreimage restrictPreimage Bundle.Pretrivialization.toPartialEquiv toPretrivialization	—	—
sourceHomeomorphBaseSetProd_apply 📖	mathematical	—	DFunLike.coe Homeomorph Set.Elem PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd toOpenPartialHomeomorph baseSet instTopologicalSpaceSubtype Set Set.instMembership EquivLike.toFunLike Homeomorph.instEquivLike sourceHomeomorphBaseSetProd mem_source toFun'	—	preimageHomeomorph_apply subset_rfl Set.instReflSubset mem_source
sourceHomeomorphBaseSetProd_symm_apply 📖	mathematical	—	DFunLike.coe Homeomorph Set.Elem baseSet PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd toOpenPartialHomeomorph instTopologicalSpaceSubtype Set Set.instMembership EquivLike.toFunLike Homeomorph.instEquivLike Homeomorph.symm sourceHomeomorphBaseSetProd OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm sourceHomeomorphBaseSetProd_symm_apply.aux	—	—
source_eq 📖	mathematical	—	PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd toOpenPartialHomeomorph Set.preimage baseSet	—	—
source_inter_preimage_target_inter 📖	mathematical	—	Set Set.instInter PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd toOpenPartialHomeomorph Set.preimage toFun' PartialEquiv.target	—	OpenPartialHomeomorph.source_inter_preimage_target_inter
symm_apply 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	symm Bundle.TotalSpace.proj OpenPartialHomeomorph.toFun' Bundle.TotalSpace instTopologicalSpaceProd OpenPartialHomeomorph.symm toOpenPartialHomeomorph symm_coe_proj Bundle.TotalSpace.snd	—	—
symm_apply_apply 📖	mathematical	Bundle.TotalSpace Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd toOpenPartialHomeomorph Bundle.TotalSpace.proj	OpenPartialHomeomorph.toFun' Bundle.TotalSpace instTopologicalSpaceProd OpenPartialHomeomorph.symm toOpenPartialHomeomorph Bundle.TotalSpace.proj toFun'	—	PartialEquiv.left_inv
symm_apply_apply_mk 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	symm toFun' Bundle.TotalSpace Bundle.TotalSpace.proj	—	symm_proj_apply
symm_apply_mk_proj 📖	mathematical	Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd toOpenPartialHomeomorph	OpenPartialHomeomorph.toFun' instTopologicalSpaceProd OpenPartialHomeomorph.symm toOpenPartialHomeomorph toFun'	—	Bundle.Pretrivialization.symm_apply_mk_proj
symm_apply_of_notMem 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	symm	—	—
symm_coe_proj 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	Bundle.TotalSpace.proj OpenPartialHomeomorph.toFun' Bundle.TotalSpace instTopologicalSpaceProd OpenPartialHomeomorph.symm toOpenPartialHomeomorph	—	proj_symm_apply'
symm_proj_apply 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	symm Bundle.TotalSpace.proj toFun' Bundle.TotalSpace Bundle.TotalSpace.snd	—	Bundle.Pretrivialization.symm_proj_apply
symm_trans_source_eq 📖	mathematical	—	PartialEquiv.source PartialEquiv.trans PartialEquiv.symm OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd toOpenPartialHomeomorph SProd.sprod Set Set.instSProd Set.instInter baseSet Set.univ	—	Bundle.Pretrivialization.symm_trans_source_eq
symm_trans_target_eq 📖	mathematical	—	PartialEquiv.target PartialEquiv.trans PartialEquiv.symm OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd toOpenPartialHomeomorph SProd.sprod Set Set.instSProd Set.instInter baseSet Set.univ	—	Bundle.Pretrivialization.symm_trans_target_eq
target_eq 📖	mathematical	—	PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd toOpenPartialHomeomorph SProd.sprod Set Set.instSProd baseSet Set.univ	—	—
tendsto_nhds_iff 📖	mathematical	Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd toOpenPartialHomeomorph	Filter.Tendsto nhds toFun'	—	OpenPartialHomeomorph.nhds_eq_comap_inf_principal Filter.tendsto_inf Filter.tendsto_comap_iff Prod.tendsto_iff coe_coe Filter.tendsto_principal coe_fst Iff.and Filter.tendsto_congr' Filter.Eventually.mono source_eq IsOpen.mem_nhds open_baseSet
toPretrivialization_injective 📖	mathematical	—	Bundle.Trivialization Bundle.Pretrivialization toPretrivialization	—	ext' OpenPartialHomeomorph.toPartialEquiv_injective
transFiberHomeomorph_apply 📖	mathematical	—	toFun' transFiberHomeomorph DFunLike.coe Homeomorph EquivLike.toFunLike Homeomorph.instEquivLike	—	—

Bundle.Trivialization.Simps

Definitions

Name	Category	Theorems
apply 📖	CompOp	—
symm_apply 📖	CompOp	—

Bundle.Trivialization.preimageHomeomorph_symm_apply

Definitions

Name	Category	Theorems
aux 📖	CompOp	1 math math: Bundle.Trivialization.preimageHomeomorph_symm_apply

Bundle.Trivialization.sourceHomeomorphBaseSetProd_symm_apply

Definitions

Name	Category	Theorems
aux 📖	CompOp	1 math math: Bundle.Trivialization.sourceHomeomorphBaseSetProd_symm_apply

---

← Back to Index