Registry · Theorem II.T03 established formalized

II.T03 — Fibration Structure

The fibered product tau^3 = tau^1 x_f T^2 is a non-trivial fibration: surjective projection, varying fiber, no global trivialization, and injective ABCD chart.

Book II Part 1 Ch. 6

Dependency Graph

Depends on (2)

II.D07 I.T04

Depended on by (2)

II.R30 II.T46

Lean Formalization

Module: TauLib.BookII.Interior.Tau3Fibration

Symbol: Tau.BookII.Interior.surjective_2_to_20