image_sigmaMk_subset_sigma_left — Mathlib

English

If a(i) ∈ t(i) for all i, then the set { (i, a(i)) : i ∈ s } is contained in s.sigma t.

Русский

Если для всех i выполняется a(i) ∈ t(i), то множество { (i, a(i)) : i ∈ s } вложено в s.sigma t.

LaTeX

$$$\\{(i, a(i)) : i \\in s\\} \\subseteq s \\sigma t \\quad \\text{whenever } \\forall i,\\ a(i) \\in t(i) $$$

Lean4

theorem image_sigmaMk_subset_sigma_left {a : ∀ i, α i} (ha : ∀ i, a i ∈ t i) :
    (fun i ↦ Sigma.mk i (a i)) '' s ⊆ s.sigma t :=
  image_subset_iff.2 fun _ hi ↦ ⟨hi, ha _⟩

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