Basic

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

Statistics

Metric	Count
Definitions FiberBundle, extend, homeomorphAt, trivializationAt, trivializationAt', trivializationAtlas, trivializationAtlas', FiberBundleCore, TotalSpace, baseSet, coordChange, fiberBundle, indexAt, localTriv, localTrivAsPartialEquiv, localTrivAt, proj, toTopologicalSpace, topologicalSpaceFiber, trivChange, FiberPrebundle, pretrivializationAt, pretrivializationAtlas, toFiberBundle, totalSpaceTopology, trivializationOfMemPretrivializationAtlas, MemTrivializationAtlas	27
Theorems continuousAt_totalSpace, continuousWithinAt_totalSpace, continuous_proj, continuous_totalSpaceMk, exists_trivialization_Icc_subset, extend_apply_self, isOpenMap_proj, isQuotientMap_proj, map_proj_nhds, mem_baseSet_trivializationAt, mem_baseSet_trivializationAt', mem_trivializationAt_proj_source, surjective_proj, t0Space, t1Space, t2Space, t3Space, totalSpaceMk_isClosedEmbedding, totalSpaceMk_isEmbedding, totalSpaceMk_isInducing, totalSpaceMk_isInducing', trivializationAt_proj_fst, trivialization_mem_atlas, trivialization_mem_atlas', baseSet_at, continuousOn_coordChange, continuous_const_section, continuous_proj, continuous_totalSpaceMk, coordChange_comp, coordChange_self, isOpenMap_proj, isOpen_baseSet, localTrivAsPartialEquiv_apply, localTrivAsPartialEquiv_coe, localTrivAsPartialEquiv_source, localTrivAsPartialEquiv_symm, localTrivAsPartialEquiv_target, localTrivAsPartialEquiv_trans, localTrivAt_apply, localTrivAt_apply_mk, localTrivAt_def, localTrivAt_snd, localTriv_apply, localTriv_symm_apply, mem_baseSet_at, mem_localTrivAsPartialEquiv_source, mem_localTrivAsPartialEquiv_target, mem_localTrivAt_baseSet, mem_localTrivAt_source, mem_localTrivAt_target, mem_localTriv_source, mem_localTriv_target, mem_trivChange_source, mk_mem_localTrivAt_source, open_source', continuousOn_of_comp_right, continuous_proj, continuous_symm_of_mem_pretrivializationAtlas, continuous_totalSpaceMk, continuous_trivChange, inducing_totalSpaceMk_of_inducing_comp, instMemTrivializationAtlasTrivializationOfMemPretrivializationAtlas, isOpen_source, isOpen_target_of_mem_pretrivializationAtlas_inter, mem_base_pretrivializationAt, mem_pretrivializationAt_source, pretrivialization_mem_atlas, totalSpaceMk_isInducing, totalSpaceMk_preimage_source, out, instMemTrivializationAtlasTrivializationAt, memTrivializationAtlas_iff	73
Total	100

FiberBundle

Definitions

Name	Category	Theorems
extend 📖	CompOp	9 math math: exists_contMDiffOn_extend, mdifferentiableAt_extend, contMDiffAt_extend', extend_apply_self, TensorialAt.mkHom_apply_eq_extend, IsCovariantDerivativeOn.torsion_apply_eq_extend, exists_mdifferentiableOn_extend, CovariantDerivative.torsion_apply_eq_extend, TensorialAt.mkHom₂_apply_eq_extend
homeomorphAt 📖	CompOp	—
trivializationAt 📖	CompOp	53 math math: TangentBundle.continuousLinearMapAt_model_space, VectorBundleCore.trivializationAt_symmL, mdifferentiableWithinAt_totalSpace, TangentBundle.symmL_trivializationAt, continuousAt_totalSpace, prod_trivializationAt', TangentBundle.symmL_trivializationAt_eq_core, mdifferentiableWithinAt_section, TangentBundle.continuousLinearMapAt_trivializationAt_eq_core, continuousWithinAt_totalSpace, pullback_trivializationAt', TangentBundle.trivializationAt_fst, VectorBundleCore.trivializationAt_coordChange_eq, instMemTrivializationAtlasTrivializationAt, mdifferentiableAt_totalSpace, chartedSpace_chartAt, inCoordinates_apply_eq₂, TangentBundle.trivializationAt_apply, VectorBundleCore.trivializationAt_continuousLinearMapAt, writtenInExtChartAt_trivializationAt, VectorBundle.continuousLinearEquivAt_apply, trivializationAt_model_space_apply, chartedSpace'_chartAt, Bundle.contMDiffWithinAt_totalSpace, TangentBundle.trivializationAt_source, VectorBundle.continuousLinearEquivAt_symm_apply, extChartAt, trivializationAt_proj_fst, eventually_norm_symmL_trivializationAt_self_comp_lt, hom_trivializationAt, Bundle.contMDiffAt_totalSpace, TangentBundle.continuousLinearMapAt_trivializationAt, eventually_norm_symmL_trivializationAt_comp_self_lt, eventually_norm_symmL_trivializationAt_lt, TangentBundle.trivializationAt_eq_localTriv, TangentBundle.symmL_model_space, hom_trivializationAt_source, mem_trivializationAt_proj_source, extChartAt_target, ContinuousLinearMap.inCoordinates_eq, mdifferentiableAt_section, writtenInExtChartAt_trivializationAt_symm, trivialization_mem_atlas, Bundle.contMDiffAt_section, TangentBundle.trivializationAt_baseSet, VectorBundleCore.trivializationAt, hom_trivializationAt_apply, Bundle.contMDiffWithinAt_section, hom_trivializationAt_baseSet, mem_baseSet_trivializationAt, eventually_norm_trivializationAt_lt, hom_trivializationAt_target, TangentBundle.trivializationAt_target
trivializationAt' 📖	CompOp	5 math math: trivialization_mem_atlas', mem_baseSet_trivializationAt', prod_trivializationAt', pullback_trivializationAt', Bundle.Trivial.fiberBundle_trivializationAt'
trivializationAtlas 📖	CompOp	3 math math: MemTrivializationAtlas.out, memTrivializationAtlas_iff, trivialization_mem_atlas
trivializationAtlas' 📖	CompOp	4 math math: trivialization_mem_atlas', Bundle.Trivial.fiberBundle_trivializationAtlas', pullback_trivializationAtlas', prod_trivializationAtlas'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousAt_totalSpace 📖	mathematical	—	ContinuousAt Bundle.TotalSpace Bundle.TotalSpace.proj Bundle.Trivialization.toFun' trivializationAt	—	Bundle.Trivialization.tendsto_nhds_iff mem_trivializationAt_proj_source
continuousWithinAt_totalSpace 📖	mathematical	—	ContinuousWithinAt Bundle.TotalSpace Bundle.TotalSpace.proj Bundle.Trivialization.toFun' trivializationAt	—	Bundle.Trivialization.tendsto_nhds_iff mem_trivializationAt_proj_source
continuous_proj 📖	mathematical	—	Continuous Bundle.TotalSpace Bundle.TotalSpace.proj	—	continuous_iff_continuousAt Eq.le map_proj_nhds
continuous_totalSpaceMk 📖	mathematical	—	Continuous Bundle.TotalSpace	—	Topology.IsInducing.continuous totalSpaceMk_isInducing
exists_trivialization_Icc_subset 📖	mathematical	—	Bundle.Trivialization Bundle.TotalSpace Bundle.TotalSpace.proj Set Set.instHasSubset Set.Icc PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Bundle.Trivialization.baseSet	—	mem_baseSet_trivializationAt lt_or_ge Set.Icc_eq_empty Set.left_mem_Icc Set.Icc_self isLUB_csSup LE.le.eq_or_lt mem_nhdsLE_iff_exists_mem_Ico_Ioc_subset mem_nhdsWithin_of_mem_nhds IsOpen.mem_nhds Bundle.Trivialization.open_baseSet IsLUB.exists_between le_rfl Set.subset_ite LT.lt.trans not_le mem_nhdsGE_iff_exists_mem_Ioc_Ico_subset HasSubset.Subset.trans Set.instIsTransSubset Set.Ico_subset_Icc_union_Ico Set.union_subset isOpen_Iio instClosedIciTopology OrderTopology.to_orderClosedTopology isOpen_Ioi instClosedIicTopology Disjoint.mono Set.inter_subset_right Mathlib.Tactic.Push.not_forall_eq Set.disjoint_left LE.le.trans LT.lt.le Set.Icc_subset_Ico_right LE.le.not_gt
extend_apply_self 📖	mathematical	—	extend	—	mem_baseSet_trivializationAt'
isOpenMap_proj 📖	mathematical	—	IsOpenMap Bundle.TotalSpace Bundle.TotalSpace.proj	—	IsOpenMap.of_nhds_le Eq.ge map_proj_nhds
isQuotientMap_proj 📖	mathematical	—	Topology.IsQuotientMap Bundle.TotalSpace Bundle.TotalSpace.proj	—	IsOpenMap.isQuotientMap isOpenMap_proj continuous_proj surjective_proj
map_proj_nhds 📖	mathematical	—	Filter.map Bundle.TotalSpace Bundle.TotalSpace.proj nhds	—	Bundle.Trivialization.map_proj_nhds Bundle.Trivialization.mem_source mem_baseSet_trivializationAt
mem_baseSet_trivializationAt 📖	mathematical	—	Set Set.instMembership Bundle.Trivialization.baseSet Bundle.TotalSpace Bundle.TotalSpace.proj trivializationAt	—	mem_baseSet_trivializationAt'
mem_baseSet_trivializationAt' 📖	mathematical	—	Set Set.instMembership Bundle.Trivialization.baseSet Bundle.TotalSpace Bundle.TotalSpace.proj trivializationAt'	—	—
mem_trivializationAt_proj_source 📖	mathematical	—	Bundle.TotalSpace Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd Bundle.Trivialization.toOpenPartialHomeomorph Bundle.TotalSpace.proj trivializationAt	—	Bundle.Trivialization.mem_source mem_baseSet_trivializationAt
surjective_proj 📖	mathematical	—	Bundle.TotalSpace Bundle.TotalSpace.proj	—	Bundle.Trivialization.proj_surjOn_baseSet mem_baseSet_trivializationAt
t0Space 📖	mathematical	—	T0Space	—	Homeomorph.t0Space
t1Space 📖	mathematical	—	T1Space	—	Homeomorph.t1Space
t2Space 📖	mathematical	—	T2Space	—	Homeomorph.t2Space
t3Space 📖	mathematical	—	T3Space	—	Homeomorph.t3Space
totalSpaceMk_isClosedEmbedding 📖	mathematical	—	Topology.IsClosedEmbedding Bundle.TotalSpace	—	totalSpaceMk_isEmbedding IsClosed.preimage continuous_proj isClosed_singleton
totalSpaceMk_isEmbedding 📖	mathematical	—	Topology.IsEmbedding Bundle.TotalSpace	—	totalSpaceMk_isInducing Bundle.TotalSpace.mk_injective
totalSpaceMk_isInducing 📖	mathematical	—	Topology.IsInducing Bundle.TotalSpace	—	totalSpaceMk_isInducing'
totalSpaceMk_isInducing' 📖	mathematical	—	Topology.IsInducing Bundle.TotalSpace	—	—
trivializationAt_proj_fst 📖	mathematical	—	Bundle.Trivialization.toFun' Bundle.TotalSpace Bundle.TotalSpace.proj trivializationAt	—	Bundle.Trivialization.coe_fst' mem_baseSet_trivializationAt
trivialization_mem_atlas 📖	mathematical	—	Bundle.Trivialization Bundle.TotalSpace Bundle.TotalSpace.proj Set Set.instMembership trivializationAtlas trivializationAt	—	trivialization_mem_atlas'
trivialization_mem_atlas' 📖	mathematical	—	Bundle.Trivialization Bundle.TotalSpace Bundle.TotalSpace.proj Set Set.instMembership trivializationAtlas' trivializationAt'	—	—

FiberBundleCore

Definitions

Name	Category	Theorems
TotalSpace 📖	CompOp	20 math math: mem_localTrivAt_source, localTrivAsPartialEquiv_target, localTrivAsPartialEquiv_coe, mem_localTrivAsPartialEquiv_source, baseSet_at, continuous_const_section, localTriv_apply, mem_localTriv_source, localTrivAsPartialEquiv_apply, TangentBundle.chartAt, mem_localTriv_target, isOpenMap_proj, localTrivAsPartialEquiv_source, mem_localTrivAsPartialEquiv_target, continuous_proj, TangentBundle.chartAt_toPartialEquiv, localTrivAsPartialEquiv_symm, open_source', localTrivAsPartialEquiv_trans, localTriv_symm_apply
baseSet 📖	CompOp	8 math math: isOpen_baseSet, mem_localTrivAsPartialEquiv_source, baseSet_at, mem_localTrivAsPartialEquiv_target, continuousOn_coordChange, mem_baseSet_at, VectorBundleCore.toFiberBundleCore_baseSet, mem_trivChange_source
coordChange 📖	CompOp	9 math math: VectorBundleCore.toFiberBundleCore_coordChange, coordChange_self, localTriv_apply, VectorBundleCore.coe_coordChange, localTrivAsPartialEquiv_apply, continuousOn_coordChange, coordChange_comp, localTriv_symm_apply, localTrivAt_snd
fiberBundle 📖	CompOp	—
indexAt 📖	CompOp	7 math math: VectorBundleCore.toFiberBundleCore_indexAt, localTriv_apply, localTrivAsPartialEquiv_apply, localTrivAt_def, mem_baseSet_at, localTriv_symm_apply, localTrivAt_snd
localTriv 📖	CompOp	12 math math: localTrivAsPartialEquiv_target, localTrivAsPartialEquiv_coe, baseSet_at, localTriv_apply, mem_localTriv_source, TangentBundle.chartAt, mem_localTriv_target, localTrivAsPartialEquiv_source, TangentBundle.trivializationAt_eq_localTriv, localTrivAt_def, localTrivAsPartialEquiv_symm, localTriv_symm_apply
localTrivAsPartialEquiv 📖	CompOp	10 math math: localTrivAsPartialEquiv_target, localTrivAsPartialEquiv_coe, mem_localTrivAsPartialEquiv_source, localTrivAsPartialEquiv_apply, localTrivAsPartialEquiv_source, mem_localTrivAsPartialEquiv_target, TangentBundle.chartAt_toPartialEquiv, localTrivAsPartialEquiv_symm, open_source', localTrivAsPartialEquiv_trans
localTrivAt 📖	CompOp	8 math math: mk_mem_localTrivAt_source, mem_localTrivAt_source, localTrivAt_apply, mem_localTrivAt_target, localTrivAt_def, mem_localTrivAt_baseSet, localTrivAt_apply_mk, localTrivAt_snd
proj 📖	CompOp	12 math math: localTrivAsPartialEquiv_target, localTrivAsPartialEquiv_coe, baseSet_at, localTriv_apply, mem_localTriv_source, TangentBundle.chartAt, mem_localTriv_target, isOpenMap_proj, localTrivAsPartialEquiv_source, continuous_proj, localTrivAsPartialEquiv_symm, localTriv_symm_apply
toTopologicalSpace 📖	CompOp	22 math math: mk_mem_localTrivAt_source, mem_localTrivAt_source, localTrivAsPartialEquiv_target, localTrivAsPartialEquiv_coe, baseSet_at, continuous_const_section, localTriv_apply, mem_localTriv_source, localTrivAt_apply, mem_localTrivAt_target, TangentBundle.chartAt, mem_localTriv_target, isOpenMap_proj, localTrivAsPartialEquiv_source, continuous_proj, mem_localTrivAt_baseSet, localTrivAt_apply_mk, localTrivAsPartialEquiv_symm, open_source', continuous_totalSpaceMk, localTriv_symm_apply, localTrivAt_snd
topologicalSpaceFiber 📖	CompOp	1 math math: continuous_totalSpaceMk
trivChange 📖	CompOp	2 math math: localTrivAsPartialEquiv_trans, mem_trivChange_source

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
baseSet_at 📖	mathematical	—	baseSet Bundle.Trivialization.baseSet TotalSpace toTopologicalSpace proj localTriv	—	—
continuousOn_coordChange 📖	mathematical	—	ContinuousOn instTopologicalSpaceProd coordChange SProd.sprod Set Set.instSProd Set.instInter baseSet Set.univ	—	—
continuous_const_section 📖	mathematical	coordChange	Continuous TotalSpace toTopologicalSpace	—	continuous_iff_continuousAt IsOpen.mem_nhds isOpen_baseSet mem_baseSet_at OpenPartialHomeomorph.continuousAt_iff_continuousAt_comp_left ContinuousAt.prodMk continuousAt_id continuousOn_const ContinuousOn.continuousAt ContinuousOn.congr
continuous_proj 📖	mathematical	—	Continuous TotalSpace toTopologicalSpace proj	—	FiberBundle.continuous_proj
continuous_totalSpaceMk 📖	mathematical	—	Continuous Fiber Bundle.TotalSpace topologicalSpaceFiber toTopologicalSpace	—	FiberBundle.continuous_totalSpaceMk
coordChange_comp 📖	mathematical	Set Set.instMembership Set.instInter baseSet	coordChange	—	—
coordChange_self 📖	mathematical	Set Set.instMembership baseSet	coordChange	—	—
isOpenMap_proj 📖	mathematical	—	IsOpenMap TotalSpace toTopologicalSpace proj	—	FiberBundle.isOpenMap_proj
isOpen_baseSet 📖	mathematical	—	IsOpen baseSet	—	—
localTrivAsPartialEquiv_apply 📖	mathematical	—	PartialEquiv.toFun TotalSpace localTrivAsPartialEquiv Bundle.TotalSpace.proj Fiber coordChange indexAt Bundle.TotalSpace.snd	—	—
localTrivAsPartialEquiv_coe 📖	mathematical	—	PartialEquiv.toFun TotalSpace localTrivAsPartialEquiv Bundle.Trivialization.toFun' proj toTopologicalSpace localTriv	—	—
localTrivAsPartialEquiv_source 📖	mathematical	—	PartialEquiv.source TotalSpace localTrivAsPartialEquiv OpenPartialHomeomorph.toPartialEquiv toTopologicalSpace instTopologicalSpaceProd Bundle.Trivialization.toOpenPartialHomeomorph proj localTriv	—	—
localTrivAsPartialEquiv_symm 📖	mathematical	—	PartialEquiv.symm TotalSpace localTrivAsPartialEquiv OpenPartialHomeomorph.toPartialEquiv toTopologicalSpace instTopologicalSpaceProd Bundle.Trivialization.toOpenPartialHomeomorph proj localTriv	—	—
localTrivAsPartialEquiv_target 📖	mathematical	—	PartialEquiv.target TotalSpace localTrivAsPartialEquiv OpenPartialHomeomorph.toPartialEquiv toTopologicalSpace instTopologicalSpaceProd Bundle.Trivialization.toOpenPartialHomeomorph proj localTriv	—	—
localTrivAsPartialEquiv_trans 📖	mathematical	—	PartialEquiv PartialEquiv.eqOnSourceSetoid PartialEquiv.trans TotalSpace PartialEquiv.symm localTrivAsPartialEquiv OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd trivChange	—	Set.ext coordChange_comp
localTrivAt_apply 📖	mathematical	—	Bundle.Trivialization.toFun' Bundle.TotalSpace Fiber Bundle.TotalSpace.proj toTopologicalSpace localTrivAt Bundle.TotalSpace.snd	—	localTrivAt.eq_1 localTriv_apply coordChange_self mem_baseSet_at
localTrivAt_apply_mk 📖	mathematical	—	Bundle.Trivialization.toFun' Bundle.TotalSpace Fiber Bundle.TotalSpace.proj toTopologicalSpace localTrivAt	—	localTrivAt_apply
localTrivAt_def 📖	mathematical	—	localTriv indexAt localTrivAt	—	—
localTrivAt_snd 📖	mathematical	—	Bundle.Trivialization.toFun' Bundle.TotalSpace Fiber Bundle.TotalSpace.proj toTopologicalSpace localTrivAt coordChange indexAt Bundle.TotalSpace.snd	—	—
localTriv_apply 📖	mathematical	—	Bundle.Trivialization.toFun' TotalSpace proj toTopologicalSpace localTriv Bundle.TotalSpace.proj Fiber coordChange indexAt Bundle.TotalSpace.snd	—	—
localTriv_symm_apply 📖	mathematical	—	OpenPartialHomeomorph.toFun' TotalSpace instTopologicalSpaceProd toTopologicalSpace OpenPartialHomeomorph.symm Bundle.Trivialization.toOpenPartialHomeomorph proj localTriv Fiber coordChange indexAt	—	—
mem_baseSet_at 📖	mathematical	—	Set Set.instMembership baseSet indexAt	—	—
mem_localTrivAsPartialEquiv_source 📖	mathematical	—	TotalSpace Set Set.instMembership PartialEquiv.source localTrivAsPartialEquiv baseSet Bundle.TotalSpace.proj Fiber	—	—
mem_localTrivAsPartialEquiv_target 📖	mathematical	—	Set Set.instMembership PartialEquiv.target TotalSpace localTrivAsPartialEquiv baseSet	—	localTrivAsPartialEquiv.eq_1 Set.mem_prod
mem_localTrivAt_baseSet 📖	mathematical	—	Set Set.instMembership Bundle.Trivialization.baseSet Bundle.TotalSpace Fiber toTopologicalSpace Bundle.TotalSpace.proj localTrivAt	—	localTrivAt.eq_1 baseSet_at mem_baseSet_at
mem_localTrivAt_source 📖	mathematical	—	TotalSpace Set Bundle.TotalSpace Fiber Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv toTopologicalSpace instTopologicalSpaceProd Bundle.Trivialization.toOpenPartialHomeomorph Bundle.TotalSpace.proj localTrivAt Bundle.Trivialization.baseSet	—	—
mem_localTrivAt_target 📖	mathematical	—	Set Set.instMembership PartialEquiv.target Bundle.TotalSpace Fiber OpenPartialHomeomorph.toPartialEquiv toTopologicalSpace instTopologicalSpaceProd Bundle.Trivialization.toOpenPartialHomeomorph Bundle.TotalSpace.proj localTrivAt Bundle.Trivialization.baseSet	—	Bundle.Trivialization.mem_target
mem_localTriv_source 📖	mathematical	—	TotalSpace Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv toTopologicalSpace instTopologicalSpaceProd Bundle.Trivialization.toOpenPartialHomeomorph proj localTriv Bundle.Trivialization.baseSet Bundle.TotalSpace.proj Fiber	—	—
mem_localTriv_target 📖	mathematical	—	Set Set.instMembership PartialEquiv.target TotalSpace OpenPartialHomeomorph.toPartialEquiv toTopologicalSpace instTopologicalSpaceProd Bundle.Trivialization.toOpenPartialHomeomorph proj localTriv Bundle.Trivialization.baseSet	—	Bundle.Trivialization.mem_target
mem_trivChange_source 📖	mathematical	—	Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd trivChange Set.instInter baseSet	—	trivChange.eq_1 Set.mem_prod
mk_mem_localTrivAt_source 📖	mathematical	—	Bundle.TotalSpace Fiber Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv toTopologicalSpace instTopologicalSpaceProd Bundle.Trivialization.toOpenPartialHomeomorph Bundle.TotalSpace.proj localTrivAt	—	—
open_source' 📖	mathematical	—	IsOpen TotalSpace toTopologicalSpace PartialEquiv.source localTrivAsPartialEquiv	—	IsOpen.prod isOpen_baseSet isOpen_univ Set.ext

FiberPrebundle

Definitions

Name	Category	Theorems
pretrivializationAt 📖	CompOp	5 math math: mem_pretrivializationAt_source, totalSpaceMk_isInducing, totalSpaceMk_preimage_source, mem_base_pretrivializationAt, pretrivialization_mem_atlas
pretrivializationAtlas 📖	CompOp	1 math math: pretrivialization_mem_atlas
toFiberBundle 📖	CompOp	1 math math: instMemTrivializationAtlasTrivializationOfMemPretrivializationAtlas
totalSpaceTopology 📖	CompOp	7 math math: continuous_symm_of_mem_pretrivializationAtlas, continuous_proj, inducing_totalSpaceMk_of_inducing_comp, continuous_totalSpaceMk, isOpen_source, instMemTrivializationAtlasTrivializationOfMemPretrivializationAtlas, continuousOn_of_comp_right
trivializationOfMemPretrivializationAtlas 📖	CompOp	1 math math: instMemTrivializationAtlasTrivializationOfMemPretrivializationAtlas

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousOn_of_comp_right 📖	mathematical	IsOpen ContinuousOn instTopologicalSpaceProd Bundle.TotalSpace PartialEquiv.toFun PartialEquiv.symm Bundle.Pretrivialization.toPartialEquiv Bundle.TotalSpace.proj pretrivializationAt SProd.sprod Set Set.instSProd Set.instInter Bundle.Pretrivialization.baseSet Set.univ	ContinuousOn Bundle.TotalSpace totalSpaceTopology Set.preimage Bundle.TotalSpace.proj	—	pretrivialization_mem_atlas ContinuousAt.continuousWithinAt Bundle.Trivialization.continuousAt_of_comp_right mem_base_pretrivializationAt ContinuousOn.continuousAt IsOpen.mem_nhds IsOpen.prod IsOpen.inter Bundle.Pretrivialization.open_baseSet isOpen_univ Bundle.Trivialization.coe_fst Bundle.Trivialization.mem_source Set.mem_univ
continuous_proj 📖	mathematical	—	Continuous Bundle.TotalSpace totalSpaceTopology Bundle.TotalSpace.proj	—	FiberBundle.continuous_proj
continuous_symm_of_mem_pretrivializationAtlas 📖	mathematical	Bundle.Pretrivialization Bundle.TotalSpace Bundle.TotalSpace.proj Set Set.instMembership pretrivializationAtlas	ContinuousOn Bundle.TotalSpace instTopologicalSpaceProd totalSpaceTopology PartialEquiv.toFun PartialEquiv.symm Bundle.Pretrivialization.toPartialEquiv Bundle.TotalSpace.proj PartialEquiv.target	—	preimage_nhdsWithin_coinduced' Filter.le_def nhds_mono le_iSup₂
continuous_totalSpaceMk 📖	mathematical	—	Continuous Bundle.TotalSpace totalSpaceTopology	—	pretrivialization_mem_atlas OpenPartialHomeomorph.continuous_iff_continuous_comp_left totalSpaceMk_preimage_source continuous_iff_le_induced Eq.le Topology.IsInducing.eq_induced totalSpaceMk_isInducing
continuous_trivChange 📖	mathematical	Bundle.Pretrivialization Bundle.TotalSpace Bundle.TotalSpace.proj Set Set.instMembership pretrivializationAtlas	ContinuousOn instTopologicalSpaceProd Bundle.TotalSpace Bundle.Pretrivialization.toFun' Bundle.TotalSpace.proj PartialEquiv.toFun PartialEquiv.symm Bundle.Pretrivialization.toPartialEquiv Set Set.instInter PartialEquiv.target Set.preimage PartialEquiv.source	—	—
inducing_totalSpaceMk_of_inducing_comp 📖	mathematical	Topology.IsInducing instTopologicalSpaceProd Bundle.TotalSpace Bundle.Pretrivialization.toFun' Bundle.TotalSpace.proj pretrivializationAt	Topology.IsInducing Bundle.TotalSpace totalSpaceTopology	—	Topology.IsInducing.of_codRestrict mem_pretrivializationAt_source Topology.IsInducing.of_comp pretrivialization_mem_atlas Continuous.codRestrict continuous_totalSpaceMk continuousOn_iff_continuous_restrict Bundle.Trivialization.continuousOn Set.restrict_comp_codRestrict
instMemTrivializationAtlasTrivializationOfMemPretrivializationAtlas 📖	mathematical	Bundle.Pretrivialization Bundle.TotalSpace Bundle.TotalSpace.proj Set Set.instMembership pretrivializationAtlas	MemTrivializationAtlas totalSpaceTopology toFiberBundle trivializationOfMemPretrivializationAtlas	—	—
isOpen_source 📖	mathematical	—	IsOpen Bundle.TotalSpace totalSpaceTopology PartialEquiv.source Bundle.Pretrivialization.toPartialEquiv Bundle.TotalSpace.proj	—	isOpen_iSup_iff isOpen_coinduced isOpen_induced_iff Bundle.Pretrivialization.open_target Set.ext Bundle.Pretrivialization.mem_target Bundle.Pretrivialization.mem_source Bundle.Pretrivialization.proj_symm_apply
isOpen_target_of_mem_pretrivializationAtlas_inter 📖	mathematical	Bundle.Pretrivialization Bundle.TotalSpace Bundle.TotalSpace.proj Set Set.instMembership pretrivializationAtlas	IsOpen instTopologicalSpaceProd Set Set.instInter PartialEquiv.target Bundle.TotalSpace Bundle.Pretrivialization.toPartialEquiv Bundle.TotalSpace.proj Set.preimage PartialEquiv.toFun PartialEquiv.symm PartialEquiv.source	—	continuousOn_iff' continuous_symm_of_mem_pretrivializationAtlas isOpen_source Set.inter_comm IsOpen.inter Bundle.Pretrivialization.open_target
mem_base_pretrivializationAt 📖	mathematical	—	Set Set.instMembership Bundle.Pretrivialization.baseSet Bundle.TotalSpace Bundle.TotalSpace.proj pretrivializationAt	—	—
mem_pretrivializationAt_source 📖	mathematical	—	Bundle.TotalSpace Set Set.instMembership PartialEquiv.source Bundle.Pretrivialization.toPartialEquiv Bundle.TotalSpace.proj pretrivializationAt	—	Bundle.Pretrivialization.source_eq mem_base_pretrivializationAt
pretrivialization_mem_atlas 📖	mathematical	—	Bundle.Pretrivialization Bundle.TotalSpace Bundle.TotalSpace.proj Set Set.instMembership pretrivializationAtlas pretrivializationAt	—	—
totalSpaceMk_isInducing 📖	mathematical	—	Topology.IsInducing instTopologicalSpaceProd Bundle.TotalSpace Bundle.Pretrivialization.toFun' Bundle.TotalSpace.proj pretrivializationAt	—	—
totalSpaceMk_preimage_source 📖	mathematical	—	Set.preimage Bundle.TotalSpace PartialEquiv.source Bundle.Pretrivialization.toPartialEquiv Bundle.TotalSpace.proj pretrivializationAt Set.univ	—	Set.eq_univ_of_forall mem_pretrivializationAt_source

MemTrivializationAtlas

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
out 📖	mathematical	—	Bundle.Trivialization Bundle.TotalSpace Bundle.TotalSpace.proj Set Set.instMembership FiberBundle.trivializationAtlas	—	—

(root)

Definitions

Name	Category	Theorems
FiberBundle 📖	CompData	—
FiberBundleCore 📖	CompData	—
FiberPrebundle 📖	CompData	—
MemTrivializationAtlas 📖	CompData	7 math math: instMemTrivializationAtlasTrivializationAt, FiberBundle.pullback_trivializationAtlas', memTrivializationAtlas_iff, FiberBundle.prod_trivializationAtlas', instMemTrivializationAtlasProdProd, Bundle.ContinuousLinearMap.memTrivializationAtlas, FiberPrebundle.instMemTrivializationAtlasTrivializationOfMemPretrivializationAtlas

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instMemTrivializationAtlasTrivializationAt 📖	mathematical	—	MemTrivializationAtlas FiberBundle.trivializationAt	—	FiberBundle.trivialization_mem_atlas
memTrivializationAtlas_iff 📖	mathematical	—	MemTrivializationAtlas Bundle.Trivialization Bundle.TotalSpace Bundle.TotalSpace.proj Set Set.instMembership FiberBundle.trivializationAtlas	—	—

---

← Back to Index