trans_source — Mathlib

English

The source of the composite symmetry (f.symm.trans e) is the product (e.baseSet ∩ f.baseSet) × univ.

Русский

Исходная область композиции симметрии равна произведению (baseSet ∩ baseSet) × univ.

LaTeX

$$$\bigl(f.toPartialEquiv.symm.trans e.toPartialEquiv\bigr).source=(e.baseSet\cap f.baseSet)\times\univ$$$

Lean4

theorem trans_source (e f : Pretrivialization F proj) :
    (f.toPartialEquiv.symm.trans e.toPartialEquiv).source = (e.baseSet ∩ f.baseSet) ×ˢ univ := by
  rw [PartialEquiv.trans_source, PartialEquiv.symm_source, e.target_inter_preimage_symm_source_eq]

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