mem_baseSet_trivializationAt — Mathlib

English

For every base point b, the base set of the trivialization at b contains the base point b itself, i.e., b lies in the baseSet of the trivialization at b.

Русский

Пусть b — базовая точка. Базовый набор тривиализации над b содержит саму точку b.

LaTeX

$$$b\in (\operatorname{trivializationAt}(F,E,b)).\text{baseSet}$$$

Lean4

theorem mem_baseSet_trivializationAt : b ∈ (trivializationAt F E b).baseSet :=
  mem_baseSet_trivializationAt' b

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