finite_image2 — Mathlib

English

If s ⊆ α, t ⊆ β are finite, then image2 f s t is finite.

Русский

Если s ⊆ α, t ⊆ β конечно, то image2 f s t конечно.

LaTeX

$$$ \\forall {\\alpha \\beta} {\\gamma} (f : α → β → γ) (s : Set α) (t : Set β) [Fintype s.Elem] [Fintype t.Elem], Finite (Set.image2 f s t).Elem$$

Lean4

instance finite_image2 (f : α → β → γ) (s : Set α) (t : Set β) [Finite s] [Finite t] : Finite (image2 f s t : Set γ) :=
  by
  rw [← image_prod]
  infer_instance

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