finite_prod — Mathlib

English

If Clopens X and Clopens Y are finite, then Clopens(X × Y) is finite.

Русский

Если множества Clopens X и Clopens Y конечны, то Clopens(X × Y) конечно.

LaTeX

$$$$ \text{Finite}(\mathrm{Clopens}(X \times Y)) $$$$

Lean4

instance finite_prod [Finite (Clopens X)] [Finite (Clopens Y)] : Finite (Clopens (X × Y)) :=
  by
  cases nonempty_fintype (Clopens X)
  cases nonempty_fintype (Clopens Y)
  exact .of_surjective _ surjective_finset_sup_prod

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