baseSet_at — Mathlib

English

The baseSet i is the domain on which the i-th local trivialization is defined, corresponding to the base in Trivialization.

Русский

Основание baseSet i — область определения i-й локальной тривиализации, соответствующая базису тривиализации.

LaTeX

$$$\\mathrm{baseSet\_at}(Z,i) : = Z.baseSet i$$$

Lean4

@[simp, mfld_simps]
theorem baseSet_at : Z.baseSet i = (Z.localTriv i).baseSet :=
  rfl

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