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

Pretrivialization

Definitions

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

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_mk_symm 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	toFun' symm	—	mk_symm apply_symm_apply mk_mem_target
apply_symm_apply 📖	mathematical	Set Set.instMembership PartialEquiv.target toPartialEquiv	toFun' PartialEquiv.toFun PartialEquiv.symm	—	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'	—	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 PartialEquiv.symm toPartialEquiv	—	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	—	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	—	—
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	Set.Elem Set.preimage instTopologicalSpaceSubtype Set.instMembership Set.restrictPreimage restrictPreimage	—	—
restrictPreimage_source 📖	mathematical	Set.Nonempty Set Set.instInter baseSet	PartialEquiv.source Set.Elem Set.preimage toPartialEquiv instTopologicalSpaceSubtype Set.instMembership Set.restrictPreimage restrictPreimage	—	—
restrictPreimage_target 📖	mathematical	Set.Nonempty Set Set.instInter baseSet	PartialEquiv.target Set.Elem Set.preimage toPartialEquiv instTopologicalSpaceSubtype Set.instMembership Set.restrictPreimage restrictPreimage	—	—
restrictPreimage_toFun 📖	mathematical	Set.Nonempty Set Set.instInter baseSet	PartialEquiv.toFun Set.Elem Set.preimage toPartialEquiv instTopologicalSpaceSubtype 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 PartialEquiv.toFun PartialEquiv.symm toPartialEquiv symm_coe_proj Bundle.TotalSpace.snd	—	—
symm_apply_apply 📖	mathematical	Set Set.instMembership PartialEquiv.source toPartialEquiv	PartialEquiv.toFun PartialEquiv.symm toFun'	—	PartialEquiv.left_inv
symm_apply_apply_mk 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	symm toFun'	—	symm_proj_apply
symm_apply_mk_proj 📖	mathematical	Set Set.instMembership PartialEquiv.source toPartialEquiv	PartialEquiv.toFun PartialEquiv.symm 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	PartialEquiv.toFun PartialEquiv.symm toPartialEquiv	—	proj_symm_apply'
symm_proj_apply 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	symm toFun' 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	—	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

Trivialization

Definitions

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

Trivialization.Simps

Definitions

Name	Category	Theorems
apply 📖	CompOp	—
symm_apply 📖	CompOp	—

Trivialization.preimageHomeomorph_symm_apply

Definitions

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

Trivialization.sourceHomeomorphBaseSetProd_symm_apply

Definitions

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

(root)

Definitions

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

---

← Back to Index