English
W-equivalence is preserved by the mvfunctor map; mapping both x and y by g yields equivalent results.
Русский
Эквивалентность по W сохраняется под отображением mvfunctorW map.
LaTeX
$$$\forall {\alpha \beta : TypeVec n} (g : \alpha \Rightarrow \beta) (x y : q.P.W \alpha), WEquiv x y \Rightarrow WEquiv ((q.P F).mvfunctorW.map g x) ((q.P F).mvfunctorW.map g y)$$$
Lean4
theorem wEquiv_map {α β : TypeVec n} (g : α ⟹ β) (x y : q.P.W α) : WEquiv x y → WEquiv (g <$$> x) (g <$$> y) := by
intro h;
induction h with
| ind a f' f₀ f₁ h ih => rw [q.P.w_map_wMk, q.P.w_map_wMk]; apply WEquiv.ind; exact ih
| abs a₀ f'₀ f₀ a₁ f'₁ f₁ h =>
rw [q.P.w_map_wMk, q.P.w_map_wMk]; apply WEquiv.abs
change
abs (q.P.objAppend1 a₀ (g ⊚ f'₀) fun x => q.P.wMap g (f₀ x)) =
abs (q.P.objAppend1 a₁ (g ⊚ f'₁) fun x => q.P.wMap g (f₁ x))
rw [← q.P.map_objAppend1, ← q.P.map_objAppend1, abs_map, abs_map, h]
| trans x y z _ _ ih₁ ih₂ =>
apply MvQPF.WEquiv.trans
· apply ih₁
· apply ih₂
