prod — Mathlib

English

If s and t are ThreeGPFree, then their Cartesian product s × t is ThreeGPFree.

Русский

Если s и t являются 3GPFree, то их произведение s × t тоже 3GPFree.

LaTeX

$$$$ \\text{ThreeGPFree}(s) \\to \\text{ThreeGPFree}(t) \\to \\text{ThreeGPFree}(s \\times t). $$$$

Lean4

@[to_additive ThreeAPFree.prod]
theorem prod {t : Set β} (hs : ThreeGPFree s) (ht : ThreeGPFree t) : ThreeGPFree (s ×ˢ t) := fun _ ha _ hb _ hc h ↦
  Prod.ext (hs ha.1 hb.1 hc.1 (Prod.ext_iff.1 h).1) (ht ha.2 hb.2 hc.2 (Prod.ext_iff.1 h).2)

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