singleton_seq — Mathlib

English

The sequence of a singleton set {f} with t equals the image of t under the evaluation map a ↦ f(a).

Русский

Последовательность множества с одиночным элементом {f} по t равна образу t под отображением, оценивающим a ↦ f(a).

LaTeX

$$$$ \\text{seq}({f})\,t = \\{ f(a) \\mid a \\in t \\} $$$$

Lean4

theorem singleton_seq {f : α → β} {t : Set α} : Set.seq ({ f } : Set (α → β)) t = f '' t :=
  image2_singleton_left

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