restrict_preimage_singleton — Mathlib

English

Restricting to s and taking the preimage of a singleton {r} yields s ∩ f⁻¹'{r}'.

Русский

Ограничение до s и взятие предобраза для множества {r} даёт s ∩ f⁻¹'{r}.

LaTeX

$$$\\restrict f s^{-1}({r}) = s \\cap f^{-1}({r}).$$$

Lean4

theorem restrict_preimage_singleton (f : α →ₛ β) {s : Set α} (hs : MeasurableSet s) {r : β} (hr : r ≠ 0) :
    restrict f s ⁻¹' { r } = s ∩ f ⁻¹' { r } :=
  f.restrict_preimage hs hr.symm

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