prod_inf — Mathlib

English

Let s be an upper set in α and t1, t2 be upper sets in β. The product distributes over the infimum in the second factor: s ×ˢ (t1 ⊓ t2) = (s ×ˢ t1) ⊓ (s ×ˢ t2).

Русский

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

LaTeX

$$$ s \times^{\mathrm{S}} (t_1 \sqcap t_2) = (s \times^{\mathrm{S}} t_1) \sqcap (s \times^{\mathrm{S}} t_2) $$$

Lean4

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

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