seq_def — Mathlib

English

The sequencing operation for Finset, t <*> s, equals t.sup (λ f, s.image f); it aggregates all results of applying f ∈ t to s.

Русский

Операция последовательности Finset, t <*> s, равна t.sup(λ f, s.image f); она объединяет все результаты применения f к s.

LaTeX

$$$$ t \\<*>\\, s = t.\\mathrm{sup} (\\lambda f, s.\\mathrm{image} f). $$$$

Lean4

@[simp]
theorem seq_def (s : Finset α) (t : Finset (α → β)) : t <*> s = t.sup fun f => s.image f :=
  rfl

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