mulSingle_le_mulSingle — Mathlib

English

For any index i, the i-th coordinate of the Pi product preserves order: mulSingle i a ≤ mulSingle i b iff a ≤ b.

Русский

Для любого индекса i координата i в произведении Pi сохраняет порядок: mulSingle i a ≤ mulSingle i b эквивалентно a ≤ b.

LaTeX

$$$\\forall i,\\ mulSingle_i(a) \\le mulSingle_i(b) \\iff a \\le b.$$$

Lean4

@[to_additive (attr := simp)]
theorem mulSingle_le_mulSingle : mulSingle i a ≤ mulSingle i b ↔ a ≤ b := by simp [mulSingle]

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