image_div_product

Mathlib.Algebra.Group.Pointwise.Finset.Basic

URI: https://scilib.ai/kg/mathlib#Finset.image_div_product

English

The division s / t is the image of the product s × t under the map (p1, p2) ↦ p1 / p2.

Русский

Деление s / t является изображением множества пары (x, y) ∈ s × t под отображением (x, y) ↦ x / y.

LaTeX

$$$(s \\times t) \\text{ image } (\\lambda p. p_1 / p_2) = s / t$$$

Lean4

@[to_additive]
theorem image_div_product : ((s ×ˢ t).image fun x : α × α => x.fst / x.snd) = s / t :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru