image_eq_image_mk — Mathlib

English

For Y → Z and X → Y with a fiber a of f ∘ g, the image of the composite fiber equals the image of f on the constructed fiber.

Русский

Для функций f:Y→Z, g:X→Y и волокна a от f ∘ g верно, что образ (f ∘ g) a равен образу f применённому к волокну, полученному через g.

LaTeX

$$$\forall {X Y Z} (f : Y \to Z) (g : X \to Y) (a : Function.Fiber (Function.comp f g)),\; a.image = Function.Fiber.image (Function.comp f g) a = Function.Fiber.image f (Function.Fiber.mk f (g (Function.Fiber.preimage (Function.comp f g) a)))$$

Lean4

theorem image_eq_image_mk (f : Y → Z) (g : X → Y) (a : Fiber (f ∘ g)) :
    a.image = (Fiber.mk f (g (a.preimage _))).image := by rw [← map_preimage_eq_image_map _ _ a, mk_image]

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