hom_trivializationAt_baseSet — Mathlib

English

The base set of the σ-twisted trivialization equals the intersection of the base sets of the two component trivializations.

Русский

Базовое множество σ-сложной тривиализации равно пересечению базовых множеств компонентных тривиализаций.

LaTeX

$$$\\operatorname{trivializationAt} (F_1 \\to SL[\\sigma] F_2) (\\lambda x \\mapsto E_1 x \\to SL[\\sigma] E_2 x) x_0$.baseSet $= (\\operatorname{trivializationAt} F_1 E_1 x_0).baseSet \\cap (\\operatorname{trivializationAt} F_2 E_2 x_0).baseSet$$$

Lean4

@[simp]
theorem hom_trivializationAt_baseSet (x₀ : B) :
    (trivializationAt (F₁ →SL[σ] F₂) (fun x ↦ E₁ x →SL[σ] E₂ x) x₀).baseSet =
      ((trivializationAt F₁ E₁ x₀).baseSet ∩ (trivializationAt F₂ E₂ x₀).baseSet) :=
  rfl

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