image_iSup₂ — Mathlib

English

The opensFunctor commutes with a second layer of iSup over opens.

Русский

opensFunctor совместим с еще одним уровнем iSup над множествами открытых.

LaTeX

$$$f.opensFunctor (iSup_i (iSup_j s_{ij})) = iSup_i (iSup_j (f.opensFunctor(s_{ij})))$$$

Lean4

theorem image_iSup₂ {ι : Sort*} {κ : ι → Sort*} (s : (i : ι) → κ i → X.Opens) :
    (f ''ᵁ ⨆ (i : ι), ⨆ (j : κ i), s i j) = ⨆ (i : ι), ⨆ (j : κ i), f ''ᵁ s i j :=
  by
  ext : 1
  simp [Set.image_iUnion₂]

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