finite_prod — Mathlib

English

Let s and t be sets. The product s × t is finite if and only if (s finite or t is empty) and (t finite or s is empty).

Русский

Пусть S и T — множества. Множество S × T конечно тогда и только тогда, когда (S конечно или T пусто) и (T конечно или S пусто).

LaTeX

$$$ \#(s \times t) < \infty \iff (\#s < \infty \lor t = \emptyset) \land (\#t < \infty \lor s = \emptyset) $$$

Lean4

theorem finite_prod : (s ×ˢ t).Finite ↔ (s.Finite ∨ t = ∅) ∧ (t.Finite ∨ s = ∅) := by
  simp only [← not_infinite, Set.infinite_prod, not_or, not_and_or, not_nonempty_iff_eq_empty]

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