lt_ofAdd_iff — Mathlib

English

For a ≠ 0 in WithZero (Multiplicative α), a < ofAdd b iff toAdd(unzero a) < b.

Русский

Для a ≠ 0 в WithZero (Multiplicative α) выполняется a < ofAdd b тогда и только тогда, когда toAdd(unzero a) < b.

LaTeX

$$$ a < ofAdd b \iff toAdd (unzero ha) < b $$$

Lean4

theorem lt_ofAdd_iff {a : WithZero (Multiplicative α)} {b : α} (ha : a ≠ 0) : a < ofAdd b ↔ toAdd (unzero ha) < b :=
  ⟨toAdd_unzero_lt_of_lt_ofAdd ha, lt_ofAdd_of_toAdd_unzero_lt ha⟩

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