map_preimage_singleton — Mathlib

English

For f.map g and a singleton {c}, the preimage equals the preimage under f of the set of b in the range with g(b) = c.

Русский

Для f.map g и множества {c} предобраз равен предобразу по f от множества b в диапазоне f с условиям g(b) = c.

LaTeX

$$$$ f.map\\, g^{-1}(\\{c\\}) = f^{-1}\\Big( \\uparrow\\{ b \\in f.range \\mid g(b) = c \\} \\Big). $$$$

Lean4

theorem map_preimage_singleton (f : α →ₛ β) (g : β → γ) (c : γ) :
    f.map g ⁻¹' { c } = f ⁻¹' ↑({b ∈ f.range | g b = c}) :=
  map_preimage _ _ _

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