fintypeMul — Mathlib

English

If α has a decidable equality and s,t are finite, then s * t is finite (the finiteness is preserved under pointwise product).

Русский

Если у типа α есть разрешимое равенство и множества s, t конечны, то s * t конечны (конечность сохраняется под покомпонентное произведение).

LaTeX

$$$$ s \\text{ finite} \\to t \\text{ finite} \\to (s * t) \\text{ finite} $$$$

Lean4

/-- Multiplication preserves finiteness. -/
@[to_additive /-- Addition preserves finiteness. -/
    ]
instance fintypeMul [DecidableEq α] (s t : Set α) [Fintype s] [Fintype t] : Fintype (s * t) :=
  Set.fintypeImage2 _ _ _

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