seq_def — Mathlib

English

The sequence operation on sets satisfies seq s t = ⋃ f ∈ s, f '' t, i.e., the set of values obtained by applying any function from s to elements of t.

Русский

Операция последовательности над множествами удовлетворяет seq s t = ⋃ f ∈ s, f '' t, то есть множество значений, получаемых применением любой функции из s к элементам t.

LaTeX

$$$$ \\operatorname{seq} s t = \\bigcup_{f \\in s} f'' t $$$$

Lean4

theorem seq_def {s : Set (α → β)} {t : Set α} : seq s t = ⋃ f ∈ s, f '' t := by rw [seq_eq_image2, iUnion_image_left]

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