mapsTo_iUnion₂ — Mathlib

English

MapsTo f (⋃ (i) (j), s i j) t iff ∀ i j, MapsTo f (s i j) t.

Русский

MapsTo f (⋃ (i) (j), s i j) t тогда и только тогда, когда для всех i и j выполняется MapsTo f (s i j) t.

LaTeX

$$$\\mathrm{MapsTo}\\, f\\,(\\bigcup_{i,j} s_{i,j})\\, t \\iff \\forall i,j, \\mathrm{MapsTo}\\, f\\,(s_{i,j})\\, t$$$

Lean4

theorem mapsTo_iUnion₂ {s : ∀ i, κ i → Set α} {t : Set β} {f : α → β} :
    MapsTo f (⋃ (i) (j), s i j) t ↔ ∀ i j, MapsTo f (s i j) t :=
  iUnion₂_subset_iff

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