mapsTo_iInter₂ — Mathlib

English

For a family of sets t_i_j indexed by i and j, MapsTo f s (⋂_{i,j} t_i_j) holds iff MapsTo f s (t_i_j) for all i and j.

Русский

Для семейства множеств t_i_j, отображение f переносит s в ⋂_{i,j} t_i_j тогда и только тогда, когда переносит s в каждое t_i_j.

LaTeX

$$$f[S] \\subseteq \\bigcap_{i,j} t_{i,j} \\iff \\forall i,j,\\ f[S] \\subseteq t_{i,j}.$$$

Lean4

theorem mapsTo_iInter₂ {s : Set α} {t : ∀ i, κ i → Set β} {f : α → β} :
    MapsTo f s (⋂ (i) (j), t i j) ↔ ∀ i j, MapsTo f s (t i j) := by simp only [mapsTo_iInter]

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