prod — Mathlib

English

If s and t are subsingleton sets, then their Cartesian product s × t is also subsingleton.

Русский

Если множества s и t — подподмножества одного элемента, то их параллельное произведение s × t тоже подподмножество одного элемента.

LaTeX

$$$s.Subsingleton \\land t.Subsingleton \\Rightarrow (s \\times\\! t).Subsingleton$$$

Lean4

theorem prod (hs : s.Subsingleton) (ht : t.Subsingleton) : (s ×ˢ t).Subsingleton := fun _x hx _y hy ↦
  Prod.ext (hs hx.1 hy.1) (ht hx.2 hy.2)

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