restrict_preimage — Mathlib

English

Restrict f to s and preimage under t equals intersection: restrict f s ⁻¹' t = s ∩ f ⁻¹' t, when s is measurable and 0 ∉ t.

Русский

Ограничение f на s и предобразование под t эквивалентны пересечению: restrict f s ⁻¹' t = s ∩ f ⁻¹' t, если s измеримо и 0 не принадлежит t.

LaTeX

$$$\\restrict f s^{-1}(t) = s \\cap f^{-1}(t)$, при измеримости s и $0 \\notin t$.$$

Lean4

theorem restrict_preimage (f : α →ₛ β) {s : Set α} (hs : MeasurableSet s) {t : Set β} (ht : (0 : β) ∉ t) :
    restrict f s ⁻¹' t = s ∩ f ⁻¹' t := by simp [hs, indicator_preimage_of_notMem _ _ ht, inter_comm]

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