preimage_sigmaMap_sigma — Mathlib

English

Let α' be a family of types and f : ι → ι' and g : ∀ i, α i → α'(f i). Then the preimage of s.sigma t under Sigma.map f g equals (preimage f s).sigma (i ↦ preimage (g i) (t (f i))).

Русский

Пусть α' - семейство типов, f : ι → ι' и g : ∀ i, α i → α'(f i). Тогда прообраз под Sigma.map f g от s.sigma t равен (preimage 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 preimage_sigmaMap_sigma {α' : ι' → Type*} (f : ι → ι') (g : ∀ i, α i → α' (f i)) (s : Set ι')
    (t : ∀ i, Set (α' i)) : Sigma.map f g ⁻¹' s.sigma t = (f ⁻¹' s).sigma fun i ↦ g i ⁻¹' t (f i) :=
  rfl

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