image₂_def — Mathlib

English

For a function f: α → β → γ and Finsets s ⊆ α, t ⊆ β, image₂ f s t equals the set { f(a,b) : a ∈ s, b ∈ t }.

Русский

Для функции f: α → β → γ и Finset s ⊆ α, t ⊆ β image₂ f s t совпадает с множеством { f(a,b) : a ∈ s, b ∈ t }.

LaTeX

$$$$ \\operatorname{image}_2 f s t = \\{\, f(a,b) : a \\in s,\\; b \\in t \\,\\}. $$$$

Lean4

/-- `Finset.image₂` in terms of monadic operations. Note that this can't be taken as the definition
because of the lack of universe polymorphism. -/
theorem image₂_def {α β γ : Type u} (f : α → β → γ) (s : Finset α) (t : Finset β) : image₂ f s t = f <$> s <*> t :=
  by
  ext
  simp [mem_sup]

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