English
The local trivialization is extended to a full trivialization by registering in its type that it is a local bundle trivialization, with the same source/target and coordinate-change data.
Русский
Локальная тривиализация расширяется до полной тривиализации, регистрируя в её типе, что она локальная тривиализация биндела, с теми же данными источника/пункта назначения и координатного изменения.
LaTeX
$$$\\text{localTriv}(i):=\\text{Trivialization}(F, Z.proj)\\quad\\text{with baseSet }=Z.baseSet i,\\ \\text{open_source}=Z.open_source'(i),\\ \\text{toPartialEquiv}=Z.localTrivAsPartialEquiv i.$$$
Lean4
theorem open_source' (i : ι) : IsOpen (Z.localTrivAsPartialEquiv i).source :=
by
apply TopologicalSpace.GenerateOpen.basic
simp only [exists_prop, mem_iUnion, mem_singleton_iff]
refine ⟨i, Z.baseSet i ×ˢ univ, (Z.isOpen_baseSet i).prod isOpen_univ, ?_⟩
ext p
simp only [localTrivAsPartialEquiv_apply, prodMk_mem_set_prod_eq, mem_inter_iff, and_self_iff,
mem_localTrivAsPartialEquiv_source, and_true, mem_univ, mem_preimage]
