eq_one_or_eq_zero_of_le_mul — Mathlib

English

For i, j in the unit interval, if i ≤ j·i then i = 0 or j = 1.

Русский

Для любых i, j из единичного интервала, если i ≤ j·i, то i = 0 или j = 1.

LaTeX

$$$$ i \\le j i \\Rightarrow i = 0 \\lor j = 1. $$$$

Lean4

theorem eq_one_or_eq_zero_of_le_mul {i j : I} (h : i ≤ j * i) : i = 0 ∨ j = 1 :=
  by
  contrapose! h
  rw [← unitInterval.lt_one_iff_ne_one, ← coe_lt_one, ← unitInterval.pos_iff_ne_zero, ← coe_pos] at h
  rw [← Subtype.coe_lt_coe, coe_mul]
  simpa using mul_lt_mul_of_pos_right h.right h.left

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