image_div — Mathlib

English

For s, t finite subsets of α, and a hom f, the image of the quotient s/t under f equals the quotient of the images: image f (s/t) = image f(s) / image f(t).

Русский

Для конечных подмножеств s, t группы α и гомоморфизма f выполняется: образ деления s/t под f равен делению образов: image f (s/t) = image f(s) / image f(t).

LaTeX

$$$\operatorname{image}(f)(s/t) = \operatorname{image}(f)(s) / \operatorname{image}(f)(t)$$$

Lean4

theorem image_div : (s / t).image (f : α → β) = s.image f / t.image f :=
  image_image₂_distrib <| map_div f

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