prod — Mathlib

English

If s ⊆ α and t ⊆ β are sup-closed, then the product s × t ⊆ α × β is sup-closed, with the join taken coordinatewise.

Русский

Если s и t замкнуты по ⊔ в α и β соответственно, то их произведение s × t ⊆ α × β также замкнуто по ⊔ на координатах.

LaTeX

$$$ (\\forall (a,b) \\in s \\times t)(\\forall (a',b') \\in s \\times t)\\, (a,b) \\sqcup (a',b') \\in s \\times t $$$

Lean4

theorem prod {t : Set β} (hs : SupClosed s) (ht : SupClosed t) : SupClosed (s ×ˢ t) := fun _a ha _b hb ↦
  ⟨hs ha.1 hb.1, ht ha.2 hb.2⟩

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