Documentation Verification Report

IsHomeomorphicTrivialBundle

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

Statistics

Metric	Count
Definitions `IsHomeomorphicTrivialFiberBundle`	1
Theorems `continuous_proj`, `isOpenMap_proj`, `isQuotientMap_proj`, `proj_eq`, `surjective_proj`, `isHomeomorphicTrivialFiberBundle_fst`, `isHomeomorphicTrivialFiberBundle_snd`	7
Total	8

IsHomeomorphicTrivialFiberBundle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_proj` 📖	mathematical	`IsHomeomorphicTrivialFiberBundle`	`Continuous`	—	`proj_eq` `Continuous.comp` `continuous_fst` `Homeomorph.continuous`
`isOpenMap_proj` 📖	mathematical	`IsHomeomorphicTrivialFiberBundle`	`IsOpenMap`	—	`proj_eq` `IsOpenMap.comp` `isOpenMap_fst` `Homeomorph.isOpenMap`
`isQuotientMap_proj` 📖	mathematical	`IsHomeomorphicTrivialFiberBundle`	`Topology.IsQuotientMap`	—	`IsOpenMap.isQuotientMap` `isOpenMap_proj` `continuous_proj` `surjective_proj`
`proj_eq` 📖	mathematical	`IsHomeomorphicTrivialFiberBundle`	`DFunLike.coe` `Homeomorph` `instTopologicalSpaceProd` `EquivLike.toFunLike` `Homeomorph.instEquivLike`	—	—
`surjective_proj` 📖	—	`IsHomeomorphicTrivialFiberBundle`	—	—	`proj_eq` `Prod.fst_surjective` `Homeomorph.surjective`

(root)

Definitions

Name	Category	Theorems
`IsHomeomorphicTrivialFiberBundle` 📖	MathDef	4 math math: `isHomeomorphicTrivialFiberBundle_snd`, `Complex.isHomeomorphicTrivialFiberBundle_re`, `isHomeomorphicTrivialFiberBundle_fst`, `Complex.isHomeomorphicTrivialFiberBundle_im`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isHomeomorphicTrivialFiberBundle_fst` 📖	mathematical	—	`IsHomeomorphicTrivialFiberBundle` `instTopologicalSpaceProd`	—	—
`isHomeomorphicTrivialFiberBundle_snd` 📖	mathematical	—	`IsHomeomorphicTrivialFiberBundle` `instTopologicalSpaceProd`	—	—

---

← Back to Index