prod — Mathlib

English

If s ⊆ α and t ⊆ β are Sublattices, then their product s × t is a Sublattice of α × β.

Русский

Если s ⊆ α и t ⊆ β — субрешетки, то их произведение s × t является субрешеткой множества α × β.

LaTeX

$$IsSublattice s → IsSublattice t → IsSublattice (Set.prod s t)$$

Lean4

theorem prod {t : Set β} (hs : IsSublattice s) (ht : IsSublattice t) : IsSublattice (s ×ˢ t) :=
  ⟨hs.1.prod ht.1, hs.2.prod ht.2⟩

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