seq — Mathlib

English

seq s t is the union of f '' t over all f ∈ s; i.e., the image2 of the evaluation map.

Русский

seq s t является объединением f''t по всем f ∈ s; то есть образование функции применения.

LaTeX

$$$$ \\text{seq}(s,t) = \\operatorname{image2}(\\lambda f\\, a \\mapsto f(a))\\, s\\, t $$$$

Lean4

/-- Given a set `s` of functions `α → β` and `t : Set α`, `seq s t` is the union of `f '' t` over
all `f ∈ s`. -/
def seq (s : Set (α → β)) (t : Set α) : Set β :=
  image2 (fun f ↦ f) s t

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