le_iff_exists_one_le_mul — Mathlib

English

Equivalence a ≤ b with existence of 1 ≤ c and a·c = b under left-mono and reflect LE.

Русский

Эквивалентность a ≤ b с существованием 1 ≤ c и a·c = b при левом монотонном и отражении LE.

LaTeX

$$$\le\;\text{iff}\;\exists c\,(1\le c \land a c = b)$. $$

Lean4

@[to_additive]
theorem le_iff_exists_one_le_mul [MulLeftMono α] [MulLeftReflectLE α] : a ≤ b ↔ ∃ c, 1 ≤ c ∧ a * c = b :=
  ⟨exists_one_le_mul_of_le, by rintro ⟨c, hc, rfl⟩; exact le_mul_of_one_le_right' hc⟩

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