English
For ENNReal a,b,c with a ≠ 0 ∨ b ≠ ∞ and a ≠ ∞ ∨ b ≠ 0, if ∀ a' > a, ∀ b' > b, c ≤ a' * b' then c ≤ a * b.
Русский
Пусть a,b,c ∈ ENNReal с условиями a ≠ 0 ∨ b ≠ ∞ и a ≠ ∞ ∨ b ≠ 0; если ∀ a' > a, ∀ b' > b выполняется c ≤ a' b', тогда c ≤ a b.
LaTeX
$$$$ \forall a,b,c \in \mathbb{R}_{\ge 0}^{\infty},\ (a \neq 0 \lor b \neq \infty) \Rightarrow \ (a \neq \infty \lor b \neq 0) \Rightarrow (\forall a' > a, \forall b' > b, c \le a' b') \Rightarrow c \le a b. $$$$
Lean4
theorem le_mul_of_forall_lt {a b c : ℝ≥0∞} (h₁ : a ≠ 0 ∨ b ≠ ∞) (h₂ : a ≠ ∞ ∨ b ≠ 0)
(h : ∀ a' > a, ∀ b' > b, c ≤ a' * b') : c ≤ a * b :=
by
rw [← ENNReal.inv_le_inv, ENNReal.mul_inv h₁ h₂]
exact
mul_le_of_forall_lt fun a' ha' b' hb' ↦
ENNReal.le_inv_iff_le_inv.1 <|
(h _ (ENNReal.lt_inv_iff_lt_inv.1 ha') _ (ENNReal.lt_inv_iff_lt_inv.1 hb')).trans_eq
(ENNReal.mul_inv (Or.inr hb'.ne_top) (Or.inl ha'.ne_top)).symm
