of_prod_right — Mathlib

English

If the Cartesian product s × t is finite, and s is nonempty, then t is finite.

Русский

Если произведение множеств s × t конечное, и s непусто, то t конечно.

LaTeX

$$$ \#(s \times t) < \infty \Rightarrow s \neq \varnothing \Rightarrow \#t < \infty $$$

Lean4

theorem of_prod_right (h : (s ×ˢ t : Set (α × β)).Finite) : s.Nonempty → t.Finite := fun ⟨a, ha⟩ =>
  (h.image Prod.snd).subset fun b hb => ⟨(a, b), ⟨ha, hb⟩, rfl⟩

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