mem_localTrivAt_baseSet — Mathlib

English

For every b in the base space B, the base set of the local trivialization at b contains the base point b.

Русский

Для каждого b в базовом пространстве B множество основания локальной тривиализации в точке b содержит саму точку b.

LaTeX

$$$ \forall b : B,\ b \in (Z.localTrivAt\ b).baseSet$$$

Lean4

@[simp, mfld_simps]
theorem mem_localTrivAt_baseSet (b : B) : b ∈ (Z.localTrivAt b).baseSet :=
  by
  rw [localTrivAt, ← baseSet_at]
  exact Z.mem_baseSet_at b

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