English
The inverse image W under a whiskered functor equals the original W after whiskering, showing compatibility of the image under left whiskering.
Русский
Обратное изображение W под функторной оберткой по левой стрелке равно исходному W после обертки, демонстрирует совместимость образа.
LaTeX
$$W_inverseImage_whiskeringLeft: K.W.inverseImage ((whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op) = J.W$$
Lean4
instance [((equivSmallModel C).inverse.inducedTopology J).WEqualsLocallyBijective A] : J.WEqualsLocallyBijective A :=
WEqualsLocallyBijective.transport J ((equivSmallModel C).inverse.inducedTopology J) (equivSmallModel C).inverse
(IsDenseSubsite.coverPreserving _ _ _)
