English
If F and G are fiberwise equivalences, then the induced sigma-congruence satisfies: (sigmaCongrRight F).trans (sigmaCongrRight G) = sigmaCongrRight (λ a, (F a).trans (G a)).
Русский
Если для каждого a дано эквивалентность по волокнам F(a) и 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
theorem sigmaCongrRight_trans {α} {β₁ β₂ β₃ : α → Type*} (F : ∀ a, β₁ a ≃ β₂ a) (G : ∀ a, β₂ a ≃ β₃ a) :
(sigmaCongrRight F).trans (sigmaCongrRight G) = sigmaCongrRight fun a => (F a).trans (G a) :=
rfl
