sigma_preimage_left — Mathlib

English

The left-side preimage of a sigma set equals the sigma-preimage under a left map: ((f⁻¹' s).sigma t) = (fun p => ⟨f p.fst, p.snd⟩)⁻¹' s.sigma t.

Русский

Левый прообраз сигмы равен соответствующему сигма-предобразованию: ((f⁻¹' s).sigma t) = (⟨f p.fst, p.snd⟩)⁻¹' s.sigma t.

LaTeX

$$$((f^{-1}' s).sigma t) = (\lambda p: \langle f p.fst, p.snd \rangle)^{-1}' (s.\sigma t)$$$

Lean4

theorem sigma_preimage_left {f : ι' → ι} :
    ((f ⁻¹' s).sigma fun i ↦ t (f i)) = (fun p : Σ i, α (f i) ↦ Sigma.mk _ p.2) ⁻¹' s.sigma t :=
  rfl

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