mem_trivializationAt_proj_source — Mathlib

English

The base point x.proj lies in the source of the trivialization at x.proj.

Русский

Базовая точка x.proj принадлежит источнику тривиализации над x.proj.

LaTeX

$$$x\in (\operatorname{trivializationAt}(F,E,x.proj)).\text{source}$$$

Lean4

@[simp, mfld_simps]
theorem mem_trivializationAt_proj_source {x : TotalSpace F E} : x ∈ (trivializationAt F E x.proj).source :=
  (Trivialization.mem_source _).mpr <| mem_baseSet_trivializationAt F E x.proj

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