iUnion_image_preimage_sigma_mk_eq_self

English

For any s : Set (Sigma σ), the union over i of image (Sigma.mk i) (preimage (Sigma.mk i) s) equals s.

Русский

Для любого s : Set (Sigma σ) объединение по i изображения (Sigma.mk i) от предобраза (Sigma.mk i) s равно s.

LaTeX

$$$$ \\bigcup_{i} \\mathrm{image}(\\mathrm{Sigma.mk} i) ( \\mathrm{preimage}(\\mathrm{Sigma.mk} i) s ) = s. $$$$

Lean4

theorem iUnion_image_preimage_sigma_mk_eq_self {ι : Type*} {σ : ι → Type*} (s : Set (Sigma σ)) :
    ⋃ i, Sigma.mk i '' (Sigma.mk i ⁻¹' s) = s := by
  ext x
  simp only [mem_iUnion, mem_image, mem_preimage]
  grind

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