English
The product of the pushforwards of atTop along u1 and u2 equals the pushforward of the product map Prod.map u1 u2 along atTop.
Русский
Произведение отображений-образов atTop через u1 и u2 равно отображению atTop через произведение отображений Prod.map u1 u2.
LaTeX
$$$\\operatorname{SProd.sprod}(\\operatorname{map} u_1\\, \\operatorname{atTop})\\, (\\operatorname{map} u_2\\, \\operatorname{atTop}) = \\operatorname{map}(\\operatorname{Prod.map} u_1\\, u_2)\\, \\operatorname{atTop}$$$
Lean4
theorem prod_map_atTop_eq {α₁ α₂ β₁ β₂ : Type*} [Preorder β₁] [Preorder β₂] (u₁ : β₁ → α₁) (u₂ : β₂ → α₂) :
map u₁ atTop ×ˢ map u₂ atTop = map (Prod.map u₁ u₂) atTop := by
rw [prod_map_map_eq, prod_atTop_atTop_eq, Prod.map_def]
