totalSpaceMk_preimage_source — Mathlib

English

The preimage of the local pretrivialization source under TotalSpace.mk b is the whole fiber, i.e., equals univ.

Русский

Предобраз источника локальной предтривиализации под TotalSpace.mk b равен всего волокну (univ).

LaTeX

$$$ (\mathrm{TotalSpace.mk}\ b)^{-1}((a.pretrivializationAt b).source) = \mathsf{univ} $$$

Lean4

@[simp]
theorem totalSpaceMk_preimage_source (b : B) : TotalSpace.mk b ⁻¹' (a.pretrivializationAt b).source = univ :=
  eq_univ_of_forall (a.mem_pretrivializationAt_source b)

Похожие утверждения