prod_self_le_prod_self

Mathlib.Order.UpperLower.Prod

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

English

The relation s1 ×ˢ s1 ≤ s2 ×ˢ s2 is equivalent to s1 ≤ s2.

Русский

Отношение s1 ×ˢ s1 ≤ s2 ×ˢ s2 эквивалентно s1 ≤ s2.

LaTeX

$$$ s_1 \times^{\mathrm{S}} s_1 \le s_2 \times^{\mathrm{S}} s_2 \;\Longleftrightarrow\; s_1 \le s_2 $$$

Lean4

@[simp]
theorem prod_self_le_prod_self : s₁ ×ˢ s₁ ≤ s₂ ×ˢ s₂ ↔ s₁ ≤ s₂ :=
  prod_self_subset_prod_self

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

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

Разделы

Аффилиация

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