fintypeProd — Mathlib

English

If s ⊆ α and t ⊆ β with s and t finite, then the product set s ×ˢ t is finite.

Русский

Если s ⊆ α и t ⊆ β и s и t конечны, то множество s ×ˢ t конечно.

LaTeX

$$$ [Fintype s] [Fintype t] : Fintype (s \\timesˢ t : Set (\\alpha \\times \\beta)) $$$

Lean4

instance fintypeProd (s : Set α) (t : Set β) [Fintype s] [Fintype t] : Fintype (s ×ˢ t : Set (α × β)) :=
  Fintype.ofFinset (s.toFinset ×ˢ t.toFinset) <| by simp

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