one_le_mulSingle — Mathlib

English

The same Pi-coordinate order equivalence for the canonical one-inequality form: mulSingle i a ≤ mulSingle i b iff a ≤ b.

Русский

Та же эквивалентность порядка по координате 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) single_nonneg]
theorem one_le_mulSingle : 1 ≤ mulSingle i a ↔ 1 ≤ a := by simp [mulSingle]

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