sigmaCongrRight_trans — Mathlib

English

The transitive composition of fiberwise equivalences F and G yields a sigma-congruence: (sigmaCongrRight F).trans (sigmaCongrRight G) = sigmaCongrRight (λ a, (F a).trans (G a)).

Русский

Транзитивное произведение эквивалентностей по волокнам порождает сигма-конгруэнтность: (sigmaCongrRight F).trans (sigmaCongrRight G) = sigmaCongrRight (λ a, (F a).trans (G a)).

LaTeX

$$$$(\sigmaCongrRight F).\text{trans}(\sigmaCongrRight G) = \sigmaCongrRight (\lambda a, (F a).trans (G a)).$$$$

Lean4

@[simp]
theorem sigmaCongrRight_trans {α} {β : α → Sort _} (F : ∀ a, Perm (β a)) (G : ∀ a, Perm (β a)) :
    (sigmaCongrRight F).trans (sigmaCongrRight G) = sigmaCongrRight fun a => (F a).trans (G a) :=
  rfl

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