image_div_prod — Mathlib

English

Let s and t be subsets. The image of the product set s × t under the map (x,y) ↦ x / y equals the quotient set s / t; i.e., ( { (x,y) | x ∈ s, y ∈ t } ) maps to x/y gives s/t.

Русский

Пусть S и T — подмножества. Образ произведения S × T при отображении (x,y) ↦ x/y равен множеству деления S/T; то есть { x/y | x ∈ S, y ∈ T } = S/T.

LaTeX

$$$ (x,y) \mapsto x/y \,[ s \times t ] = s/t $$$

Lean4

@[to_additive sub_image_prod]
theorem image_div_prod : (fun x : α × α => x.fst / x.snd) '' s ×ˢ t = s / t :=
  image_prod _

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