product — Mathlib

English

If s and t are nonempty Finsets, then s × t is nonempty.

Русский

Если s и t не пусты, то s × t не пустое.

LaTeX

$$$(s \\\\neq \\\\emptyset) \\\\land (t \\\\neq \\\\emptyset) \\\\Rightarrow (s \\\\times t) \\\\neq \\\\emptyset$$$

Lean4

@[aesop safe apply (rule_sets := [finsetNonempty])]
theorem product (hs : s.Nonempty) (ht : t.Nonempty) : (s ×ˢ t).Nonempty :=
  let ⟨x, hx⟩ := hs
  let ⟨y, hy⟩ := ht
  ⟨(x, y), mem_product.2 ⟨hx, hy⟩⟩

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