Basic

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

Statistics

Metric	Count
Definitions FiberBundle, trivializationAt, trivializationAt', trivializationAtlas, trivializationAtlas', FiberBundleCore, TotalSpace, baseSet, coordChange, fiberBundle, indexAt, localTriv, localTrivAsPartialEquiv, localTrivAt, proj, toTopologicalSpace, topologicalSpaceFiber, trivChange, FiberPrebundle, pretrivializationAt, pretrivializationAtlas, toFiberBundle, totalSpaceTopology, trivializationOfMemPretrivializationAtlas, MemTrivializationAtlas	25
Theorems continuousAt_totalSpace, continuousWithinAt_totalSpace, continuous_proj, continuous_totalSpaceMk, exists_trivialization_Icc_subset, isOpenMap_proj, isQuotientMap_proj, map_proj_nhds, mem_baseSet_trivializationAt, mem_baseSet_trivializationAt', mem_trivializationAt_proj_source, surjective_proj, 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	68
Total	93

FiberBundle

Definitions

Name	Category	Theorems
trivializationAt 📖	CompOp	46 math math: TangentBundle.continuousLinearMapAt_model_space, 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, instMemTrivializationAtlasTrivializationAt, mdifferentiableAt_totalSpace, chartedSpace_chartAt, TangentBundle.trivializationAt_apply, writtenInExtChartAt_trivializationAt, trivializationAt_model_space_apply, chartedSpace'_chartAt, Bundle.contMDiffWithinAt_totalSpace, TangentBundle.trivializationAt_source, 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, 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 Trivialization.toFun' trivializationAt	—	Trivialization.tendsto_nhds_iff mem_trivializationAt_proj_source
continuousWithinAt_totalSpace 📖	mathematical	—	ContinuousWithinAt Bundle.TotalSpace Bundle.TotalSpace.proj Trivialization.toFun' trivializationAt	—	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	—	Set Set.instHasSubset Set.Icc PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Trivialization.baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	—	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 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
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	—	Trivialization.map_proj_nhds Trivialization.mem_source mem_baseSet_trivializationAt
mem_baseSet_trivializationAt 📖	mathematical	—	Set Set.instMembership Trivialization.baseSet Bundle.TotalSpace Bundle.TotalSpace.proj trivializationAt	—	mem_baseSet_trivializationAt'
mem_baseSet_trivializationAt' 📖	mathematical	—	Set Set.instMembership Trivialization.baseSet Bundle.TotalSpace Bundle.TotalSpace.proj trivializationAt'	—	—
mem_trivializationAt_proj_source 📖	mathematical	—	Bundle.TotalSpace Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd Trivialization.toOpenPartialHomeomorph Bundle.TotalSpace.proj trivializationAt	—	Trivialization.mem_source mem_baseSet_trivializationAt
surjective_proj 📖	mathematical	—	Bundle.TotalSpace Bundle.TotalSpace.proj	—	Trivialization.proj_surjOn_baseSet mem_baseSet_trivializationAt
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	—	Trivialization.toFun' Bundle.TotalSpace Bundle.TotalSpace.proj trivializationAt	—	Trivialization.coe_fst' mem_baseSet_trivializationAt
trivialization_mem_atlas 📖	mathematical	—	Trivialization Bundle.TotalSpace Bundle.TotalSpace.proj Set Set.instMembership trivializationAtlas trivializationAt	—	trivialization_mem_atlas'
trivialization_mem_atlas' 📖	mathematical	—	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 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 Trivialization.toFun' proj toTopologicalSpace localTriv	—	—
localTrivAsPartialEquiv_source 📖	mathematical	—	PartialEquiv.source TotalSpace localTrivAsPartialEquiv OpenPartialHomeomorph.toPartialEquiv toTopologicalSpace instTopologicalSpaceProd Trivialization.toOpenPartialHomeomorph proj localTriv	—	—
localTrivAsPartialEquiv_symm 📖	mathematical	—	PartialEquiv.symm TotalSpace localTrivAsPartialEquiv OpenPartialHomeomorph.toPartialEquiv toTopologicalSpace instTopologicalSpaceProd Trivialization.toOpenPartialHomeomorph proj localTriv	—	—
localTrivAsPartialEquiv_target 📖	mathematical	—	PartialEquiv.target TotalSpace localTrivAsPartialEquiv OpenPartialHomeomorph.toPartialEquiv toTopologicalSpace instTopologicalSpaceProd 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	—	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	—	Trivialization.toFun' Bundle.TotalSpace Fiber Bundle.TotalSpace.proj toTopologicalSpace localTrivAt	—	localTrivAt_apply
localTrivAt_def 📖	mathematical	—	localTriv indexAt localTrivAt	—	—
localTrivAt_snd 📖	mathematical	—	Trivialization.toFun' Bundle.TotalSpace Fiber Bundle.TotalSpace.proj toTopologicalSpace localTrivAt coordChange indexAt Bundle.TotalSpace.snd	—	—
localTriv_apply 📖	mathematical	—	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 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 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 Trivialization.toOpenPartialHomeomorph Bundle.TotalSpace.proj localTrivAt Trivialization.baseSet	—	—
mem_localTrivAt_target 📖	mathematical	—	Set Set.instMembership PartialEquiv.target Bundle.TotalSpace Fiber OpenPartialHomeomorph.toPartialEquiv toTopologicalSpace instTopologicalSpaceProd Trivialization.toOpenPartialHomeomorph Bundle.TotalSpace.proj localTrivAt Trivialization.baseSet	—	Trivialization.mem_target
mem_localTriv_source 📖	mathematical	—	TotalSpace Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv toTopologicalSpace instTopologicalSpaceProd Trivialization.toOpenPartialHomeomorph proj localTriv Trivialization.baseSet Bundle.TotalSpace.proj Fiber	—	—
mem_localTriv_target 📖	mathematical	—	Set Set.instMembership PartialEquiv.target TotalSpace OpenPartialHomeomorph.toPartialEquiv toTopologicalSpace instTopologicalSpaceProd Trivialization.toOpenPartialHomeomorph proj localTriv Trivialization.baseSet	—	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 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 Pretrivialization.toPartialEquiv Bundle.TotalSpace.proj pretrivializationAt SProd.sprod Set Set.instSProd Set.instInter Pretrivialization.baseSet Set.univ	totalSpaceTopology Set.preimage	—	pretrivialization_mem_atlas ContinuousAt.continuousWithinAt Trivialization.continuousAt_of_comp_right mem_base_pretrivializationAt ContinuousOn.continuousAt IsOpen.mem_nhds IsOpen.prod IsOpen.inter Pretrivialization.open_baseSet isOpen_univ Trivialization.coe_fst 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	Pretrivialization Bundle.TotalSpace Bundle.TotalSpace.proj Set Set.instMembership pretrivializationAtlas	ContinuousOn instTopologicalSpaceProd totalSpaceTopology PartialEquiv.toFun PartialEquiv.symm Pretrivialization.toPartialEquiv 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	Pretrivialization Bundle.TotalSpace Bundle.TotalSpace.proj Set Set.instMembership pretrivializationAtlas	ContinuousOn instTopologicalSpaceProd Pretrivialization.toFun' PartialEquiv.toFun PartialEquiv.symm Pretrivialization.toPartialEquiv Set.instInter PartialEquiv.target Set.preimage PartialEquiv.source	—	—
inducing_totalSpaceMk_of_inducing_comp 📖	mathematical	Topology.IsInducing instTopologicalSpaceProd Bundle.TotalSpace Pretrivialization.toFun' Bundle.TotalSpace.proj pretrivializationAt	totalSpaceTopology	—	Topology.IsInducing.of_codRestrict mem_pretrivializationAt_source Topology.IsInducing.of_comp pretrivialization_mem_atlas Continuous.codRestrict continuous_totalSpaceMk continuousOn_iff_continuous_restrict Trivialization.continuousOn Set.restrict_comp_codRestrict
instMemTrivializationAtlasTrivializationOfMemPretrivializationAtlas 📖	mathematical	Pretrivialization Bundle.TotalSpace Bundle.TotalSpace.proj Set Set.instMembership pretrivializationAtlas	MemTrivializationAtlas totalSpaceTopology toFiberBundle trivializationOfMemPretrivializationAtlas	—	—
isOpen_source 📖	mathematical	—	IsOpen Bundle.TotalSpace totalSpaceTopology PartialEquiv.source Pretrivialization.toPartialEquiv Bundle.TotalSpace.proj	—	isOpen_iSup_iff isOpen_coinduced isOpen_induced_iff Pretrivialization.open_target Set.ext Pretrivialization.mem_target Pretrivialization.mem_source Pretrivialization.proj_symm_apply
isOpen_target_of_mem_pretrivializationAtlas_inter 📖	mathematical	Pretrivialization Bundle.TotalSpace Bundle.TotalSpace.proj Set Set.instMembership pretrivializationAtlas	IsOpen instTopologicalSpaceProd Set.instInter PartialEquiv.target Pretrivialization.toPartialEquiv Set.preimage PartialEquiv.toFun PartialEquiv.symm PartialEquiv.source	—	continuousOn_iff' continuous_symm_of_mem_pretrivializationAtlas isOpen_source Set.inter_comm IsOpen.inter Pretrivialization.open_target
mem_base_pretrivializationAt 📖	mathematical	—	Set Set.instMembership Pretrivialization.baseSet Bundle.TotalSpace Bundle.TotalSpace.proj pretrivializationAt	—	—
mem_pretrivializationAt_source 📖	mathematical	—	Bundle.TotalSpace Set Set.instMembership PartialEquiv.source Pretrivialization.toPartialEquiv Bundle.TotalSpace.proj pretrivializationAt	—	Pretrivialization.source_eq mem_base_pretrivializationAt
pretrivialization_mem_atlas 📖	mathematical	—	Pretrivialization Bundle.TotalSpace Bundle.TotalSpace.proj Set Set.instMembership pretrivializationAtlas pretrivializationAt	—	—
totalSpaceMk_isInducing 📖	mathematical	—	Topology.IsInducing instTopologicalSpaceProd Bundle.TotalSpace Pretrivialization.toFun' Bundle.TotalSpace.proj pretrivializationAt	—	—
totalSpaceMk_preimage_source 📖	mathematical	—	Set.preimage Bundle.TotalSpace PartialEquiv.source 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	—	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 Trivialization Bundle.TotalSpace Bundle.TotalSpace.proj Set Set.instMembership FiberBundle.trivializationAtlas	—	—

---

← Back to Index