English
Let ei be a family of PartialEquiv (α_i i) → (β_i i) and ei' a family (β_i i) → (γ_i i). Then the composition of the π-constructions equals the π-construction of the componentwise compositions: (PartialEquiv.pi ei).trans (PartialEquiv.pi ei') = PartialEquiv.pi (i ↦ (ei i).trans (ei' i)).
Русский
Пусть ei — семейство PartialEquiv (α_i i) → (β_i i), и ei' — семейство (β_i i) → (γ_i i). Тогда композицияPi-конструкций равна Pi-конструкции компонентно-композиций: (PartialEquiv.pi ei).trans (PartialEquiv.pi ei') = PartialEquiv.pi (i ↦ (ei i).trans (ei' i)).
LaTeX
$$$\\left(\\PartialEquiv.pi\\, ei\\right).\\text{trans}\\left(\\PartialEquiv.pi\\, ei'\\right) = \\PartialEquiv.pi\\;\\lambda i. (ei\,i).\\text{trans} (ei'\,i)$$$
Lean4
@[simp, mfld_simps]
theorem pi_trans (ei : ∀ i, PartialEquiv (αi i) (βi i)) (ei' : ∀ i, PartialEquiv (βi i) (γi i)) :
(PartialEquiv.pi ei).trans (PartialEquiv.pi ei') = .pi fun i ↦ (ei i).trans (ei' i) := by ext <;> simp [forall_and]
