inf_prod — Mathlib

English

Let s1, s2 be lower sets in α and t be a lower set in β. The product distributes over the infimum in the second 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 inter_prod

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