image_sigmaMk_preimage_sigmaMap — Mathlib

English

If f is injective, then the previous subset becomes equality.

Русский

Если f инъективен, то вложение превращается в равенство.

LaTeX

$$$\\text{Injective } f \\Rightarrow\\ (\\\\Sigma.mk i '' (g i^{-1}' s) = (\\\\Sigma.map f g)^{-1}' (\\\\Sigma.mk (f i) '' s))$$$

Lean4

theorem image_sigmaMk_preimage_sigmaMap {β : ι' → Type*} {f : ι → ι'} (hf : Function.Injective f)
    (g : ∀ i, α i → β (f i)) (i : ι) (s : Set (β (f i))) :
    Sigma.mk i '' (g i ⁻¹' s) = Sigma.map f g ⁻¹' (Sigma.mk (f i) '' s) :=
  by
  refine (image_sigmaMk_preimage_sigmaMap_subset f g i s).antisymm ?_
  rintro ⟨j, x⟩ ⟨y, hys, hxy⟩
  simp only [hf.eq_iff, Sigma.map, Sigma.ext_iff] at hxy
  grind

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