prod_self_lt_prod_self — Mathlib

English

The strict order on products reflects the strict order of each coordinate: s1 × s1 < s2 × s2 iff s1 < s2.

Русский

Строгое отношение на произведении отражает строгое отношение по каждой координате: s1 × s1 < s2 × s2 ⇔ s1 < s2.

LaTeX

$$$ s_1 \\times s_1 < s_2 \\times 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

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