Ici_product_Ici — Mathlib

English

In the product of two ordered sets, the lower interval from (a, b) is exactly the product of the lower intervals from a and b.

Русский

В произведении упорядоченных множеств нижний интервал от (a, b) равен произведению нижних интервалов от a и b.

LaTeX

$$$ (\mathrm{Ici}\ a) \times (\mathrm{Ici}\ b) = \mathrm{Ici}\ (a,b) $$$

Lean4

theorem Ici_product_Ici (a : α) (b : β) : Ici a ×ˢ Ici b = Ici (a, b) :=
  rfl

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