range_prod — Mathlib

English

Let I and J be ModelWithCorners. Then the image of the product map I.prod J equals the strong product of the images: range (I.prod J) = range I ×ˢ range J.

Русский

Пусть I и J — модели с углами. Тогда образ произведения отображений I.prod J равен сильному произведению образов: range (I.prod J) = range I ×ˢ range J.

LaTeX

$$$\mathrm{range}((I.prod J).toFun') = \mathrm{Set}.instSProd.sprod(\mathrm{range} I.toFun', \mathrm{range} J.toFun')$$$

Lean4

theorem range_prod : range (I.prod J) = range I ×ˢ range J := by simp_rw [← ModelWithCorners.target_eq]; rfl

Похожие утверждения