continuous_proj — Mathlib

English

Projection map from the vector bundle built from the core to the base space is continuous.

Русский

Переходная проекция из векторного расслоения, построенного из ядра, в базовую пространство непрерывна.

LaTeX

$$$Z.proj\; \text{ is continuous}$$$

Lean4

/-- The projection on the base of a vector bundle created from core is continuous -/
@[continuity]
theorem continuous_proj : Continuous Z.proj :=
  Z.toFiberBundleCore.continuous_proj

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