English
If f: α × β → γ is a function and s ⊆ α, t ⊆ β are finite, then image2 f s t is finite.
Русский
Если f: α × β → γ и s ⊆ α, t ⊆ β конечны, то image2 f s t конечно.
LaTeX
$$$ [\\text{DecidableEq } \\gamma] (f : α \\to β \\to \\gamma) (s : Set \\alpha) (t : Set \\beta) [hs : Fintype s] [ht : Fintype t] \\Rightarrow Fintype (image2 f s t : Set \\gamma) $$
Lean4
/-- `image2 f s t` is `Fintype` if `s` and `t` are. -/
instance fintypeImage2 [DecidableEq γ] (f : α → β → γ) (s : Set α) (t : Set β) [hs : Fintype s] [ht : Fintype t] :
Fintype (image2 f s t : Set γ) := by
rw [← image_prod]
apply Set.fintypeImage