sigma_preimage_right — Mathlib

English

The right-side preimage of a sigma set equals the preimage under Sigma.map: (s.sigma (i ↦ g i⁻¹' t i)) = (λ p, ⟨p.1, g p.1 p.2⟩)⁻¹' s.sigma t.

Русский

Правый предобраз сигмы равен прообразованию под Sigma.map: (s.sigma (i ↦ g i⁻¹' t i)) = (λ p, ⟨p.1, g p.1 p.2⟩)⁻¹' s.sigma t.

LaTeX

$$$(s.\sigma (\lambda i. g_i^{-1}' t_i)) = (\lambda p. \langle p.1, g p.1 p.2 \rangle)^{-1}' (s.\sigma t)$$$

Lean4

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

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