mul_le_of_forall_lt — Mathlib

English

For ENNReal a,b,c, if for all a' > a and b' > b we have c ≤ a' * b', then c ≤ a * b.

Русский

Для ENNReal a,b,c: если для всех a' > a и b' > b выполняется c ≤ a' b', то c ≤ a b.

LaTeX

$$$$ \forall a,b,c \in \mathbb{R}_{\ge 0}^{\infty},\ (\forall a' > a,\ \forall b' > b,\ c \le a' b') \Rightarrow c \le a b. $$$$

Lean4

theorem mul_le_of_forall_lt {a b c : ℝ≥0∞} (h : ∀ a' < a, ∀ b' < b, a' * b' ≤ c) : a * b ≤ c :=
  by
  refine le_of_forall_lt_imp_le_of_dense fun d hd ↦ ?_
  obtain ⟨a', ha', hd⟩ := exists_lt_mul_left hd
  obtain ⟨b', hb', hd⟩ := exists_lt_mul_right hd
  exact le_trans hd.le <| h _ ha' _ hb'

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