mapsTo_sInter — Mathlib

English

Let s ⊆ α, T a collection of subsets of β, and f: α → β. Then MapsTo f s (⋂ T) holds iff MapsTo f s t for every t ∈ T.

Русский

Пусть s ⊆ α, T — семейство подмножеств β, и f: α → β. Тогда MapsTo f s (⋂ T) эквивалентно MapsTo f s t для каждого t ∈ T.

LaTeX

$$$\\operatorname{MapsTo}(f,s,\\bigcap T) \\iff \\forall t \\in T, \\operatorname{MapsTo}(f,s,t).$$$

Lean4

@[simp]
theorem mapsTo_sInter {s : Set α} {T : Set (Set β)} {f : α → β} : MapsTo f s (⋂₀ T) ↔ ∀ t ∈ T, MapsTo f s t :=
  forall₂_swap

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