Theorems · Theorem · combinatorics

Set.Finite.toFinset_image2

∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {s : Set α} {t : Set β} (f : α → β → γ)
  (hs : s.Finite) (ht : t.Finite) (hf : optParam (Set.image2 f s t).Finite ⋯),
  hf.toFinset = Finset.image₂ f hs.toFinset ht.toFinset

Defined in

Mathlib.Data.Finset.NAry

Cited by

5 results in Mathlib

Foundations

Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEq