mem_source_at — Mathlib

English

The point (b, a) lies in the source of the trivialization at i; i.e., it's within the domain where the trivialization is defined.

Русский

Точка (b, a) принадлежит источнику тривиализации i, то есть находится в области определения тривиализации.

LaTeX

$$$(\langle b, a \rangle) \in (Z.localTriv i).source$$$

Lean4

@[simp, mfld_simps]
theorem mem_source_at : (⟨b, a⟩ : Z.TotalSpace) ∈ (Z.localTrivAt b).source :=
  by
  rw [localTrivAt, mem_localTriv_source]
  exact Z.mem_baseSet_at b

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