lean_workbook_plus_75235
DisprovedShow that
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_75235 : ∀ m M : ℝ, ∀ θ : ℝ, (1 / ((1 - θ) * m + θ * M) ≤ (1 - θ) / m + θ / M) := by sorry
Source
Show that
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_75235 : ∀ m M : ℝ, ∀ θ : ℝ, (1 / ((1 - θ) * m + θ * M) ≤ (1 - θ) / m + θ / M) := by sorry