fintypeImage2 — Mathlib

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

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