inf_prod — Mathlib

English

Let s1, s2 be upper sets in α and t be an upper set in β. The product distributes over the infimum in the first factor: (s1 ⊓ s2) ×ˢ t = (s1 ×ˢ t) ⊓ (s2 ×ˢ t).

Русский

Пусть s1, s2 — верхние множества на α, а t — верхнее множество на β. Произведение распределяется по пересечению в первой компоненте: (s1 ⊓ s2) ×ˢ t = (s1 ×ˢ t) ⊓ (s2 ×ˢ t).

LaTeX

$$$ (s_1 \sqcap s_2) \times^{\mathrm{S}} t = (s_1 \times^{\mathrm{S}} t) \sqcap (s_2 \times^{\mathrm{S}} t) $$$

Lean4

@[simp]
theorem inf_prod : (s₁ ⊓ s₂) ×ˢ t = s₁ ×ˢ t ⊓ s₂ ×ˢ t :=
  ext union_prod

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