Lean4
/-- The product of a family of partial equivalences, as a partial equivalence on the pi type. -/
@[simps (attr := mfld_simps) -fullyApplied apply source target]
protected def pi (ei : ∀ i, PartialEquiv (αi i) (βi i)) : PartialEquiv (∀ i, αi i) (∀ i, βi i)
where
toFun := Pi.map fun i ↦ ei i
invFun := Pi.map fun i ↦ (ei i).symm
source := pi univ fun i => (ei i).source
target := pi univ fun i => (ei i).target
map_source' _ hf i hi := (ei i).map_source (hf i hi)
map_target' _ hf i hi := (ei i).map_target (hf i hi)
left_inv' _ hf := funext fun i => (ei i).left_inv (hf i trivial)
right_inv' _ hf := funext fun i => (ei i).right_inv (hf i trivial)
