map_preimage — Mathlib

English

For a simple function f and a function g, the preimage under f.map g of a set s equals the preimage under f of the corresponding set of b in the range of f with g(b) ∈ s.

Русский

Для простой функции f и отображения g, предобраз по f.map g множества s равен предобразу по f от соответствующего множества b в диапазоне f с условием g(b) ∈ s.

LaTeX

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

Lean4

theorem map_preimage (f : α →ₛ β) (g : β → γ) (s : Set γ) : f.map g ⁻¹' s = f ⁻¹' ↑({b ∈ f.range | g b ∈ s}) :=
  by
  simp only [coe_range, sep_mem_eq, coe_map, Finset.coe_filter, ← mem_preimage, inter_comm, preimage_inter_range,
    ← Finset.mem_coe]
  exact preimage_comp

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