image_sigmaMk_preimage_sigmaMap_subset

English

For i, g, f, the image of the preimage under g_i is contained in the preimage under Sigma.map of the image under Sigma.mk (f i).

Русский

Для i, g, f выполняется вложение: образ предобраза по g_i содержится в предобразе под Sigma.map f g от образа Sigma.mk (f i)'' s.

LaTeX

$$$\\Sigma.mk i '' (g i^{-1}' s) \\subseteq \\Sigma.map f g^{-1}' (\\Sigma.mk (f i) '' s)$$$

Lean4

theorem image_sigmaMk_preimage_sigmaMap_subset {β : ι' → Type*} (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) :=
  image_subset_iff.2 fun x hx ↦ ⟨g i x, hx, rfl⟩

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