sigmaCongrRight — Mathlib

English

An equivalence e: α1 ≃ α2 induces an equivalence between Σ a1, β (f a) and Σ a2, β a.

Русский

Эквивалентность e: α1 ≃ α2 порождает эквивалентность между Σ a1, β (e a) и Σ a2, β a.

LaTeX

$$$${\text{sigmaCongrLeft }(e): (\Sigma a_1, \beta (e a)) \cong \Sigma a_2, \beta a.}$$$$

Lean4

/-- A family of permutations `Π a, Perm (β a)` generates a permutation `Perm (Σ a, β₁ a)`. -/
abbrev sigmaCongrRight {α} {β : α → Sort _} (F : ∀ a, Perm (β a)) : Perm (Σ a, β a) :=
  Equiv.sigmaCongrRight F

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