map_preimage_eq_image_map — Mathlib

English

For a fiber a of (g ∘ f), g(f(a.preimage)) equals a.image.

Русский

Для волокна a от композиции g ∘ f верно g(f(a.preimage)) = a.image.

LaTeX

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

Lean4

theorem map_preimage_eq_image_map {W : Type*} (f : Y → Z) (g : Z → W) (a : Fiber (g ∘ f)) :
    g (f a.preimage) = a.image := by rw [← map_preimage_eq_image, comp_apply]

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