exists_of_lt_mul — Mathlib

English

If c < a*b, then there exist a' < a and b' < b such that a'*b + a*b' + a'*b' = c.

Русский

Если c < a*b, то существуют a' < a и b' < b такие, что a'*b + a*b' + a'*b' = c.

LaTeX

$$$ c < a b \Rightarrow \exists a' < a, \exists b' < b, a' b + a b' + a' b' = c$$$

Lean4

theorem exists_of_lt_mul (h : c < a * b) : ∃ a' < a, ∃ b' < b, a' * b + a * b' + a' * b' = c :=
  by
  rw [mul_def] at h
  have := notMem_of_lt_csInf' h
  rwa [Set.notMem_compl_iff] at this

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