mapsTo_iInter — Mathlib

English

A set of the form ⋂ i t_i; f maps s into that intersection iff f maps s into each t_i.

Русский

Пересечение по всем i: отображение f переносит s в ⋂_i t_i тогда и только тогда, когда переносит s в каждое t_i.

LaTeX

$$$f[S] \\subseteq \\bigcap_i t_i \\iff \\forall i,\\ f[S] \\subseteq t_i.$$$

Lean4

@[simp]
theorem mapsTo_iInter {s : Set α} {t : ι → Set β} {f : α → β} : MapsTo f s (⋂ i, t i) ↔ ∀ i, MapsTo f s (t i) :=
  mapsTo_sInter.trans forall_mem_range

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