zeroSection — Mathlib

English

Under a linear trivialization, the image of the zero section is the base point paired with the zero vector in the model fiber.

Русский

Под линейной тривиализацией образ нулевой секции сопоставляется точке базы пара (база, нулевой вектор в модели фибры).

LaTeX

$$$e(\text{zeroSection } F E\, x) = (x, 0)$ for all x in the baseSet$$

Lean4

protected theorem zeroSection (e : Trivialization F (π F E)) [e.IsLinear R] {x : B} (hx : x ∈ e.baseSet) :
    e (zeroSection F E x) = (x, 0) := by
  simp_rw [zeroSection, e.apply_eq_prod_continuousLinearEquivAt R x hx 0, map_zero]

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