mem_pretrivializationAt_source — Mathlib

English

For every b in B and x in E(b), the pair (b,x) lies in the source of the pretrivialization at b.

Русский

Для каждого b в B и x в E(b) пара (b,x) принадлежит источнику предтривиализации при b.

LaTeX

$$$ \langle b, x \rangle \in (a.pretrivializationAt b).source \quad \text{for all } b \in B, x \in E(b) $$$

Lean4

theorem mem_pretrivializationAt_source (b : B) (x : E b) : ⟨b, x⟩ ∈ (a.pretrivializationAt b).source :=
  by
  simp only [(a.pretrivializationAt b).source_eq, mem_preimage]
  exact a.mem_base_pretrivializationAt b

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