Documentation Verification Report

Constructions

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

Statistics

Metric	Count
Definitions `fiberBundle`, `homeomorphProd`, `topologicalSpace`, `trivialization`, `topologicalSpace`, `prod`, `pullback`, `topologicalSpace`, `invFun'`, `toFun'`, `prod`, `pullback`, `instTopologicalSpacePullback`, `pullbackTopology`	14
Theorems `eq_trivialization`, `fiberBundle_trivializationAt'`, `fiberBundle_trivializationAtlas'`, `homeomorphProd_apply`, `homeomorphProd_symm_apply_proj`, `homeomorphProd_symm_apply_snd`, `isInducing_toProd`, `toOpenPartialHomeomorph_trivialization_symm_apply`, `trivialization_apply`, `trivialization_baseSet`, `trivialization_source`, `trivialization_symm_apply`, `trivialization_symm_apply_proj`, `trivialization_symm_apply_snd`, `trivialization_target`, `isInducing_diag`, `prod_trivializationAt'`, `prod_trivializationAtlas'`, `pullback_trivializationAt'`, `pullback_trivializationAtlas'`, `continuous_lift`, `continuous_proj`, `continuous_totalSpaceMk`, `continuous_inv_fun`, `continuous_to_fun`, `left_inv`, `right_inv`, `prod_apply`, `prod_baseSet`, `prod_source`, `prod_symm_apply`, `prod_symm_apply_proj`, `prod_symm_apply_snd`, `prod_target`, `pullback_apply`, `pullback_baseSet`, `pullback_source`, `pullback_symm_apply_proj`, `pullback_symm_apply_snd`, `pullback_target`, `inducing_pullbackTotalSpaceEmbedding`, `instMemTrivializationAtlasProdProd`, `pullbackTopology_def`	43
Total	57

Bundle.Trivial

Definitions

Name	Category	Theorems
`fiberBundle` 📖	CompOp	13 math math: `continuousLinearEquivAt_trivialization`, `Bundle.ContMDiffRiemannianMetric.contMDiff`, `symmL_trivialization`, `continuousLinearMapAt_trivialization`, `fiberBundle_trivializationAtlas'`, `instIsContinuousRiemannianBundleTrivial`, `vectorBundle`, `Bundle.ContinuousRiemannianMetric.continuous`, `IsContMDiffRiemannianBundle.exists_contMDiff`, `IsContinuousRiemannianBundle.exists_continuous`, `instIsContMDiffRiemannianBundleTrivial`, `fiberBundle_trivializationAt'`, `contMDiffVectorBundle`
`homeomorphProd` 📖	CompOp	3 math math: `homeomorphProd_symm_apply_snd`, `homeomorphProd_symm_apply_proj`, `homeomorphProd_apply`
`topologicalSpace` 📖	CompOp	29 math math: `continuousLinearEquivAt_trivialization`, `Bundle.ContMDiffRiemannianMetric.contMDiff`, `symmL_trivialization`, `continuousLinearMapAt_trivialization`, `fiberBundle_trivializationAtlas'`, `instIsContinuousRiemannianBundleTrivial`, `vectorBundle`, `Bundle.ContinuousRiemannianMetric.continuous`, `isInducing_toProd`, `trivialization_target`, `linearMapAt_trivialization`, `IsContMDiffRiemannianBundle.exists_contMDiff`, `trivialization_symm_apply`, `homeomorphProd_symm_apply_snd`, `IsContinuousRiemannianBundle.exists_continuous`, `trivialization_apply`, `trivialization.isLinear`, `toOpenPartialHomeomorph_trivialization_symm_apply`, `homeomorphProd_symm_apply_proj`, `instIsContMDiffRiemannianBundleTrivial`, `fiberBundle_trivializationAt'`, `contMDiffVectorBundle`, `trivialization.coordChangeL`, `symmₗ_trivialization`, `trivialization_baseSet`, `trivialization_symm_apply_proj`, `homeomorphProd_apply`, `trivialization_source`, `trivialization_symm_apply_snd`
`trivialization` 📖	CompOp	18 math math: `continuousLinearEquivAt_trivialization`, `symmL_trivialization`, `eq_trivialization`, `continuousLinearMapAt_trivialization`, `fiberBundle_trivializationAtlas'`, `trivialization_target`, `linearMapAt_trivialization`, `trivialization_symm_apply`, `trivialization_apply`, `trivialization.isLinear`, `toOpenPartialHomeomorph_trivialization_symm_apply`, `fiberBundle_trivializationAt'`, `trivialization.coordChangeL`, `symmₗ_trivialization`, `trivialization_baseSet`, `trivialization_symm_apply_proj`, `trivialization_source`, `trivialization_symm_apply_snd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_trivialization` 📖	mathematical	—	`trivialization`	—	`MemTrivializationAtlas.out`
`fiberBundle_trivializationAt'` 📖	mathematical	—	`FiberBundle.trivializationAt'` `Bundle.Trivial` `topologicalSpace` `fiberBundle` `trivialization`	—	—
`fiberBundle_trivializationAtlas'` 📖	mathematical	—	`FiberBundle.trivializationAtlas'` `Bundle.Trivial` `topologicalSpace` `fiberBundle` `Trivialization` `Bundle.TotalSpace` `Bundle.TotalSpace.proj` `Set` `Set.instSingletonSet` `trivialization`	—	—
`homeomorphProd_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `Bundle.TotalSpace` `Bundle.Trivial` `topologicalSpace` `instTopologicalSpaceProd` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `homeomorphProd` `Bundle.TotalSpace.proj` `Bundle.TotalSpace.snd`	—	—
`homeomorphProd_symm_apply_proj` 📖	mathematical	—	`Bundle.TotalSpace.proj` `DFunLike.coe` `Homeomorph` `Bundle.TotalSpace` `Bundle.Trivial` `instTopologicalSpaceProd` `topologicalSpace` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `Homeomorph.symm` `homeomorphProd`	—	—
`homeomorphProd_symm_apply_snd` 📖	mathematical	—	`Bundle.TotalSpace.snd` `DFunLike.coe` `Homeomorph` `Bundle.TotalSpace` `Bundle.Trivial` `instTopologicalSpaceProd` `topologicalSpace` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `Homeomorph.symm` `homeomorphProd`	—	—
`isInducing_toProd` 📖	mathematical	—	`Topology.IsInducing` `Bundle.TotalSpace` `topologicalSpace` `instTopologicalSpaceProd` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Bundle.TotalSpace.toProd`	—	`induced_inf` `induced_compose`
`toOpenPartialHomeomorph_trivialization_symm_apply` 📖	mathematical	—	`OpenPartialHomeomorph.toFun'` `Bundle.TotalSpace` `Bundle.Trivial` `instTopologicalSpaceProd` `topologicalSpace` `OpenPartialHomeomorph.symm` `Trivialization.toOpenPartialHomeomorph` `Bundle.TotalSpace.proj` `trivialization`	—	—
`trivialization_apply` 📖	mathematical	—	`Trivialization.toFun'` `Bundle.TotalSpace` `Bundle.Trivial` `Bundle.TotalSpace.proj` `topologicalSpace` `trivialization` `Bundle.TotalSpace.snd`	—	—
`trivialization_baseSet` 📖	mathematical	—	`Trivialization.baseSet` `Bundle.TotalSpace` `Bundle.Trivial` `topologicalSpace` `Bundle.TotalSpace.proj` `trivialization` `Set.univ`	—	—
`trivialization_source` 📖	mathematical	—	`PartialEquiv.source` `Bundle.TotalSpace` `Bundle.Trivial` `OpenPartialHomeomorph.toPartialEquiv` `topologicalSpace` `instTopologicalSpaceProd` `Trivialization.toOpenPartialHomeomorph` `Bundle.TotalSpace.proj` `trivialization` `Set.univ`	—	—
`trivialization_symm_apply` 📖	mathematical	—	`Trivialization.symm` `Bundle.Trivial` `topologicalSpace` `trivialization`	—	—
`trivialization_symm_apply_proj` 📖	mathematical	—	`Bundle.TotalSpace.proj` `Bundle.Trivial` `OpenPartialHomeomorph.toFun'` `Bundle.TotalSpace` `instTopologicalSpaceProd` `topologicalSpace` `OpenPartialHomeomorph.symm` `Trivialization.toOpenPartialHomeomorph` `trivialization`	—	—
`trivialization_symm_apply_snd` 📖	mathematical	—	`Bundle.TotalSpace.snd` `Bundle.Trivial` `OpenPartialHomeomorph.toFun'` `Bundle.TotalSpace` `instTopologicalSpaceProd` `topologicalSpace` `OpenPartialHomeomorph.symm` `Trivialization.toOpenPartialHomeomorph` `Bundle.TotalSpace.proj` `trivialization`	—	—
`trivialization_target` 📖	mathematical	—	`PartialEquiv.target` `Bundle.TotalSpace` `Bundle.Trivial` `OpenPartialHomeomorph.toPartialEquiv` `topologicalSpace` `instTopologicalSpaceProd` `Trivialization.toOpenPartialHomeomorph` `Bundle.TotalSpace.proj` `trivialization` `Set.univ`	—	—

FiberBundle

Definitions

Name	Category	Theorems
`prod` 📖	CompOp	6 math math: `prod_trivializationAt'`, `prod_trivializationAtlas'`, `Trivialization.continuousLinearEquivAt_prod`, `instMemTrivializationAtlasProdProd`, `Bundle.Prod.contMDiffVectorBundle`, `VectorBundle.prod`
`pullback` 📖	CompOp	4 math math: `ContMDiffVectorBundle.pullback`, `pullback_trivializationAt'`, `pullback_trivializationAtlas'`, `VectorBundle.pullback`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod_trivializationAt'` 📖	mathematical	—	`trivializationAt'` `instTopologicalSpaceProd` `Prod.topologicalSpace` `prod` `Trivialization.prod` `trivializationAt`	—	—
`prod_trivializationAtlas'` 📖	mathematical	—	`trivializationAtlas'` `instTopologicalSpaceProd` `Prod.topologicalSpace` `prod` `setOf` `Trivialization` `Bundle.TotalSpace` `Bundle.TotalSpace.proj` `MemTrivializationAtlas` `Trivialization.prod`	—	—
`pullback_trivializationAt'` 📖	mathematical	—	`trivializationAt'` `Bundle.Pullback` `DFunLike.coe` `Pullback.TotalSpace.topologicalSpace` `instTopologicalSpacePullback` `pullback` `Trivialization.pullback` `trivializationAt`	—	—
`pullback_trivializationAtlas'` 📖	mathematical	—	`trivializationAtlas'` `Bundle.Pullback` `DFunLike.coe` `Pullback.TotalSpace.topologicalSpace` `instTopologicalSpacePullback` `pullback` `setOf` `Trivialization` `Bundle.TotalSpace` `Bundle.TotalSpace.proj` `MemTrivializationAtlas` `Trivialization.pullback`	—	—

FiberBundle.Prod

Definitions

Name	Category	Theorems
`topologicalSpace` 📖	CompOp	18 math math: `Trivialization.prod_apply`, `FiberBundle.prod_trivializationAt'`, `Trivialization.Prod.continuous_inv_fun`, `isInducing_diag`, `Trivialization.prod_symm_apply`, `Trivialization.prod.isLinear`, `FiberBundle.prod_trivializationAtlas'`, `Trivialization.prod_symm_apply_proj`, `Trivialization.prod_symm_apply_snd`, `Trivialization.Prod.continuous_to_fun`, `instMemTrivializationAtlasProdProd`, `Trivialization.prod_target`, `Trivialization.prod_baseSet`, `Trivialization.prod_apply'`, `Bundle.Prod.contMDiffVectorBundle`, `VectorBundle.prod`, `Trivialization.prod_source`, `Trivialization.coordChangeL_prod`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isInducing_diag` 📖	mathematical	—	`Topology.IsInducing` `Bundle.TotalSpace` `topologicalSpace` `instTopologicalSpaceProd` `Bundle.TotalSpace.proj` `Bundle.TotalSpace.snd`	—	—

Pullback

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_lift` 📖	mathematical	—	`Continuous` `Bundle.TotalSpace` `Bundle.Pullback` `TotalSpace.topologicalSpace` `Bundle.Pullback.lift`	—	`continuous_iff_le_induced` `TotalSpace.topologicalSpace.eq_1` `pullbackTopology_def` `inf_le_right`
`continuous_proj` 📖	mathematical	—	`Continuous` `Bundle.TotalSpace` `Bundle.Pullback` `TotalSpace.topologicalSpace` `Bundle.TotalSpace.proj`	—	`continuous_iff_le_induced` `TotalSpace.topologicalSpace.eq_1` `pullbackTopology_def` `inf_le_left`
`continuous_totalSpaceMk` 📖	mathematical	—	`Continuous` `Bundle.Pullback` `Bundle.TotalSpace` `instTopologicalSpacePullback` `TotalSpace.topologicalSpace`	—	`pullbackTopology_def` `induced_inf` `induced_compose` `induced_const` `top_inf_eq` `Eq.le` `Topology.IsInducing.eq_induced` `FiberBundle.totalSpaceMk_isInducing`

Pullback.TotalSpace

Definitions

Name	Category	Theorems
`topologicalSpace` 📖	CompOp	15 math math: `Trivialization.pullback_linear`, `Trivialization.pullback_source`, `Pullback.continuous_lift`, `ContMDiffVectorBundle.pullback`, `Trivialization.pullback_target`, `FiberBundle.pullback_trivializationAt'`, `FiberBundle.pullback_trivializationAtlas'`, `Pullback.continuous_proj`, `Trivialization.pullback_apply`, `Pullback.continuous_totalSpaceMk`, `Trivialization.pullback_symm_apply_snd`, `Trivialization.pullback_baseSet`, `inducing_pullbackTotalSpaceEmbedding`, `Trivialization.pullback_symm_apply_proj`, `VectorBundle.pullback`

Trivialization

Definitions

Name	Category	Theorems
`prod` 📖	CompOp	13 math math: `prod_apply`, `FiberBundle.prod_trivializationAt'`, `prod_symm_apply`, `prod.isLinear`, `FiberBundle.prod_trivializationAtlas'`, `prod_symm_apply_proj`, `prod_symm_apply_snd`, `instMemTrivializationAtlasProdProd`, `prod_target`, `prod_baseSet`, `prod_apply'`, `prod_source`, `coordChangeL_prod`
`pullback` 📖	CompOp	9 math math: `pullback_linear`, `pullback_source`, `pullback_target`, `FiberBundle.pullback_trivializationAt'`, `FiberBundle.pullback_trivializationAtlas'`, `pullback_apply`, `pullback_symm_apply_snd`, `pullback_baseSet`, `pullback_symm_apply_proj`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod_apply` 📖	mathematical	—	`toFun'` `Bundle.TotalSpace` `instTopologicalSpaceProd` `Bundle.TotalSpace.proj` `FiberBundle.Prod.topologicalSpace` `prod` `Prod.toFun'`	—	—
`prod_baseSet` 📖	mathematical	—	`baseSet` `Bundle.TotalSpace` `instTopologicalSpaceProd` `FiberBundle.Prod.topologicalSpace` `Bundle.TotalSpace.proj` `prod` `Set` `Set.instInter`	—	—
`prod_source` 📖	mathematical	—	`PartialEquiv.source` `Bundle.TotalSpace` `OpenPartialHomeomorph.toPartialEquiv` `FiberBundle.Prod.topologicalSpace` `instTopologicalSpaceProd` `toOpenPartialHomeomorph` `Bundle.TotalSpace.proj` `prod` `Set` `Set.instInter` `Set.preimage` `baseSet`	—	—
`prod_symm_apply` 📖	mathematical	—	`PartialEquiv.toFun` `Bundle.TotalSpace` `PartialEquiv.symm` `OpenPartialHomeomorph.toPartialEquiv` `FiberBundle.Prod.topologicalSpace` `instTopologicalSpaceProd` `toOpenPartialHomeomorph` `Bundle.TotalSpace.proj` `prod` `symm`	—	—
`prod_symm_apply_proj` 📖	mathematical	—	`Bundle.TotalSpace.proj` `OpenPartialHomeomorph.toFun'` `Bundle.TotalSpace` `instTopologicalSpaceProd` `FiberBundle.Prod.topologicalSpace` `OpenPartialHomeomorph.symm` `toOpenPartialHomeomorph` `prod`	—	—
`prod_symm_apply_snd` 📖	mathematical	—	`Bundle.TotalSpace.snd` `OpenPartialHomeomorph.toFun'` `Bundle.TotalSpace` `instTopologicalSpaceProd` `FiberBundle.Prod.topologicalSpace` `OpenPartialHomeomorph.symm` `toOpenPartialHomeomorph` `Bundle.TotalSpace.proj` `prod` `symm`	—	—
`prod_target` 📖	mathematical	—	`PartialEquiv.target` `Bundle.TotalSpace` `OpenPartialHomeomorph.toPartialEquiv` `FiberBundle.Prod.topologicalSpace` `instTopologicalSpaceProd` `toOpenPartialHomeomorph` `Bundle.TotalSpace.proj` `prod` `SProd.sprod` `Set` `Set.instSProd` `Set.instInter` `baseSet` `Set.univ`	—	—
`pullback_apply` 📖	mathematical	—	`toFun'` `Bundle.TotalSpace` `Bundle.Pullback` `DFunLike.coe` `Bundle.TotalSpace.proj` `Pullback.TotalSpace.topologicalSpace` `pullback` `Bundle.Pullback.lift`	—	—
`pullback_baseSet` 📖	mathematical	—	`baseSet` `Bundle.TotalSpace` `Bundle.Pullback` `DFunLike.coe` `Pullback.TotalSpace.topologicalSpace` `Bundle.TotalSpace.proj` `pullback` `Set.preimage`	—	—
`pullback_source` 📖	mathematical	—	`PartialEquiv.source` `Bundle.TotalSpace` `Bundle.Pullback` `DFunLike.coe` `OpenPartialHomeomorph.toPartialEquiv` `Pullback.TotalSpace.topologicalSpace` `instTopologicalSpaceProd` `toOpenPartialHomeomorph` `Bundle.TotalSpace.proj` `pullback` `Set.preimage` `Bundle.Pullback.lift`	—	—
`pullback_symm_apply_proj` 📖	mathematical	—	`Bundle.TotalSpace.proj` `Bundle.Pullback` `DFunLike.coe` `OpenPartialHomeomorph.toFun'` `Bundle.TotalSpace` `instTopologicalSpaceProd` `Pullback.TotalSpace.topologicalSpace` `OpenPartialHomeomorph.symm` `toOpenPartialHomeomorph` `pullback`	—	—
`pullback_symm_apply_snd` 📖	mathematical	—	`Bundle.TotalSpace.snd` `Bundle.Pullback` `DFunLike.coe` `OpenPartialHomeomorph.toFun'` `Bundle.TotalSpace` `instTopologicalSpaceProd` `Pullback.TotalSpace.topologicalSpace` `OpenPartialHomeomorph.symm` `toOpenPartialHomeomorph` `Bundle.TotalSpace.proj` `pullback` `symm`	—	—
`pullback_target` 📖	mathematical	—	`PartialEquiv.target` `Bundle.TotalSpace` `Bundle.Pullback` `DFunLike.coe` `OpenPartialHomeomorph.toPartialEquiv` `Pullback.TotalSpace.topologicalSpace` `instTopologicalSpaceProd` `toOpenPartialHomeomorph` `Bundle.TotalSpace.proj` `pullback` `SProd.sprod` `Set` `Set.instSProd` `Set.preimage` `baseSet` `Set.univ`	—	—

Trivialization.Prod

Definitions

Name	Category	Theorems
`invFun'` 📖	CompOp	3 math math: `continuous_inv_fun`, `right_inv`, `left_inv`
`toFun'` 📖	CompOp	4 math math: `Trivialization.prod_apply`, `right_inv`, `left_inv`, `continuous_to_fun`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_inv_fun` 📖	mathematical	—	`ContinuousOn` `Bundle.TotalSpace` `instTopologicalSpaceProd` `FiberBundle.Prod.topologicalSpace` `invFun'` `SProd.sprod` `Set` `Set.instSProd` `Set.instInter` `Trivialization.baseSet` `Bundle.TotalSpace.proj` `Set.univ`	—	`Topology.IsInducing.continuousOn_iff` `FiberBundle.Prod.isInducing_diag` `Continuous.prodMk` `Continuous.fst` `continuous_id'` `Continuous.snd` `ContinuousOn.comp` `ContinuousOn.prodMap` `Trivialization.continuousOn_symm` `Continuous.continuousOn` `Set.mem_univ`
`continuous_to_fun` 📖	mathematical	—	`ContinuousOn` `Bundle.TotalSpace` `FiberBundle.Prod.topologicalSpace` `instTopologicalSpaceProd` `toFun'` `Set.preimage` `Bundle.TotalSpace.proj` `Set` `Set.instInter` `Trivialization.baseSet`	—	`Topology.IsInducing.continuous` `FiberBundle.Prod.isInducing_diag` `ContinuousOn.prodMap` `OpenPartialHomeomorph.continuousOn` `Continuous.prodMk` `Continuous.fst` `continuous_id'` `Continuous.snd` `ContinuousOn.congr` `ContinuousOn.comp` `Continuous.comp_continuousOn` `Continuous.continuousOn` `Trivialization.source_eq` `Set.mapsTo_preimage` `Trivialization.coe_fst` `Set.mem_preimage`
`left_inv` 📖	mathematical	`Bundle.TotalSpace` `Set` `Set.instMembership` `Set.preimage` `Bundle.TotalSpace.proj` `Set.instInter` `Trivialization.baseSet`	`invFun'` `toFun'`	—	—
`right_inv` 📖	mathematical	`Set` `Set.instMembership` `SProd.sprod` `Set.instSProd` `Set.instInter` `Trivialization.baseSet` `Bundle.TotalSpace` `Bundle.TotalSpace.proj` `Set.univ`	`toFun'` `invFun'`	—	`Trivialization.apply_mk_symm`

(root)

Definitions

Name	Category	Theorems
`instTopologicalSpacePullback` 📖	CompOp	5 math math: `ContMDiffVectorBundle.pullback`, `FiberBundle.pullback_trivializationAt'`, `FiberBundle.pullback_trivializationAtlas'`, `Pullback.continuous_totalSpaceMk`, `VectorBundle.pullback`
`pullbackTopology` 📖	CompOp	1 math math: `pullbackTopology_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inducing_pullbackTotalSpaceEmbedding` 📖	mathematical	—	`Topology.IsInducing` `Bundle.TotalSpace` `Bundle.Pullback` `Pullback.TotalSpace.topologicalSpace` `instTopologicalSpaceProd` `Bundle.pullbackTotalSpaceEmbedding`	—	`induced_inf` `induced_compose` `pullbackTopology_def`
`instMemTrivializationAtlasProdProd` 📖	mathematical	—	`MemTrivializationAtlas` `instTopologicalSpaceProd` `FiberBundle.Prod.topologicalSpace` `FiberBundle.prod` `Trivialization.prod`	—	—
`pullbackTopology_def` 📖	mathematical	—	`pullbackTopology` `TopologicalSpace` `Bundle.TotalSpace` `Bundle.Pullback` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.instCompleteLattice` `TopologicalSpace.induced` `Bundle.TotalSpace.proj` `Bundle.Pullback.lift`	—	—

---

← Back to Index