sigma_preimage_eq — Mathlib

English

If f : ι → ι' and g : ∀ i, α i → α'(f i), then the preimage of s.sigma t under Sigma.map f g equals (f⁻¹ s) .sigma (i ↦ preimage (g i) (t (f i))).

Русский

Пусть f : ι → ι' и g : ∀ i, α i → α'(f i). Тогда прообраз подσ-мэппинга равен (f⁻¹ s) .sigma (i ↦ preimage (g i) (t (f i))).

LaTeX

$$$\Sigma\text{map} f g^{-1}(s \sigma t) = (f^{-1} s) \sigma (i \mapsto g_i^{-1}(t(f i)))$$$

Lean4

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

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