image2_div — Mathlib

English

Let s and t be subsets. The set of all quotients x / y with x ∈ s and y ∈ t is exactly the image of the product s × t under the division map (x,y) ↦ x / y; i.e., { x / y | x ∈ s, y ∈ t } = s / t.

Русский

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

LaTeX

$$$ \{ x/y \mid x \in s, y \in t \} = s / t $$$$

Lean4

@[to_additive (attr := simp)]
theorem image2_div : image2 (· / ·) s t = s / t :=
  rfl

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