Theorems · Theorem · combinatorics

Set.toFinset_image2

∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] (f : α → β → γ) (s : Set α) (t : Set β)
  [inst_1 : Fintype ↑s] [inst_2 : Fintype ↑t] [inst_3 : Fintype ↑(Set.image2 f s t)],
  (Set.image2 f s t).toFinset = Finset.image₂ f s.toFinset t.toFinset

Defined in: Mathlib.Data.Finset.NAry
Cited by: 5 results in Mathlib
Foundations: Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: DecidableEq Fintype Fintype Fintype

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
Finsetstatement · cited by 13,712
Fintypestatement and proof · cited by 7,736
Set.Elemstatement and proof · cited by 7,166
Set.image2statement and proof · cited by 311
Set.toFinsetstatement and proof · cited by 217
Finset.coe_injectiveproof · cited by 127
Finset.image₂statement and proof · cited by 104
Finset.coe_image₂proof · cited by 55
Set.coe_toFinsetproof · cited by 51

Cited by5

Results whose statement or proof uses this declaration.

Set.toFinset_mulproof · cited by 1
Set.toFinset_vaddproof · cited by 0
Set.toFinset_vsubproof · cited by 0
Set.toFinset_smulproof · cited by 0
Set.toFinset_addproof · cited by 0