sInter_image — Mathlib

English

Let f be a function from α to subsets of β, and s a subset of α. The intersection of the image f''s equals the intersection over a ∈ s of f(a): ⋂₀ (f '' s) = ⋂ a ∈ s, f a.

Русский

Пусть f: α → Set β, и s ⊆ α. Пересечение образов f''s равно пересечению по всем a ∈ s: ⋂₀ (f '' s) = ⋂ a ∈ s, f a.

LaTeX

$$$$ \\bigcap_{U \\in f''s} U = \\bigcap_{a \\in s} f(a). $$$$

Lean4

@[simp]
theorem sInter_image (f : α → Set β) (s : Set α) : ⋂₀ (f '' s) = ⋂ a ∈ s, f a :=
  sInf_image

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