Finset.image₂_def

theorem Finset.image₂_def : ∀ [inst : (P : Prop) → Decidable P] {α β γ : Type u} (f : α → β → γ) (s : Finset α) (t : Finset β), Finset.image₂ f s t = Seq.seq (f <$> s) fun x => t

The theorem `Finset.image₂_def` establishes an equivalence between the operation `Finset.image₂` and a sequence of monadic operations for any given binary function `f : α → β → γ` and two finsets `s : Finset α` and `t : Finset β`. Specifically, it states that applying `Finset.image₂` to the function `f` and the finsets `s` and `t` is the same as applying the function `f` to each element of `s` (denoted by `f <$> s`) and then sequencing this with the finset `t`. Note that this equivalence cannot be used as the definition due to the lack of universe polymorphism.

More concisely: The theorem `Finset.image₂_def` in Lean 4 establishes the equivalence between `Finset.image₂ f s t` and `f <$> s <<< t`, where `f : α → β → γ`, `s : Finset α`, and `t : Finset β`.