symm_proj_apply — Mathlib

English

The target of the composite symmetry equals the product of the base subset intersection with the universal fiber, i.e., (baseSet ∩ baseSet') × univ.

Русский

Целевой набор композиции симметрии равен произведению пересечения базовых множеств на единичную фибру.

LaTeX

$$$(e.baseSet\cap e'.baseSet)\times\univ$$$

Lean4

theorem symm_proj_apply (e : Pretrivialization F (π F E)) (z : TotalSpace F E) (hz : z.proj ∈ e.baseSet) :
    e.symm z.proj (e z).2 = z.2 := by
  rw [e.symm_apply hz, cast_eq_iff_heq, e.mk_proj_snd' hz, e.symm_apply_apply (e.mem_source.mpr hz)]

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