finite_prod — Mathlib

English

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

Русский

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

LaTeX

$$$ \\forall {\\alpha \\beta} (s : Set \\alpha) (t : Set \\beta), s.\\Finite \\land t.\\Finite \\Rightarrow (s \\timesˢ t).\\Finite $$$

Lean4

instance finite_prod (s : Set α) (t : Set β) [Finite s] [Finite t] : Finite (s ×ˢ t : Set (α × β)) :=
  Finite.of_equiv _ (Equiv.Set.prod s t).symm

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