mul_le_of_forall_ne — Mathlib

English

If for all a' < a and b' < b we have a'*b + a*b' + a'*b' ≠ c, then a*b ≤ c.

Русский

Если для всех a'<a и b'<b выполняется a'*b + a*b' + a'*b' ≠ c, то a*b ≤ c.

LaTeX

$$(\forall a' < a, \forall b' < b, a'\cdot b + a\cdot b' + a'\cdot b' \neq c) \Rightarrow a\cdot b \le c$$

Lean4

theorem mul_le_of_forall_ne (h : ∀ a' < a, ∀ b' < b, a' * b + a * b' + a' * b' ≠ c) : a * b ≤ c :=
  by
  by_contra! h'
  have := exists_of_lt_mul h'
  tauto

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