prod_self_lt_prod_self

Mathlib.Order.UpperLower.Prod

URI: https://scilib.ai/kg/mathlib#UpperSet.prod_self_lt_prod_self

English

The strict version: s1 ×ˢ s1 < s2 ×ˢ s2 iff s1 < s2.

Русский

Жесткая версия: s1 ×ˢ s1 < s2 ×ˢ s2 эквивалентно s1 < s2.

LaTeX

$$$ s_1 \times^{\mathrm{S}} s_1 < s_2 \times^{\mathrm{S}} s_2 \;\iff\; s_1 < s_2 $$$

Lean4

@[simp]
theorem prod_self_lt_prod_self : s₁ ×ˢ s₁ < s₂ ×ˢ s₂ ↔ s₁ < s₂ :=
  prod_self_ssubset_prod_self

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru