sigmaCongrLeft' — Mathlib

English

Transporting a sigma type through an equivalence of the base: (sigmaCongrLeft' f).

Русский

Перемещаем сигма-тип через эквивалентность основания: (sigmaCongrLeft' f).

LaTeX

$$$${\text{sigmaCongrLeft'}(f): (\Sigma a_1, \beta a) \cong (\Sigma a_2, \beta (f^{-1} a))}.$$$$

Lean4

/-- Transporting a sigma type through an equivalence of the base -/
def sigmaCongrLeft' {α₁ α₂} {β : α₁ → Sort _} (f : α₁ ≃ α₂) : (Σ a : α₁, β a) ≃ Σ a : α₂, β (f.symm a) :=
  (sigmaCongrLeft f.symm).symm

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