lean_workbook_plus_77864
ProvedSo exist and and
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_77864 : ∃ a b : ℝ, a ≤ 1 ∧ b ≥ 1 ∧ (1 - a) * (1 - b) ≤ 1 := by sorry
Source
So exist and and
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_77864 : ∃ a b : ℝ, a ≤ 1 ∧ b ≥ 1 ∧ (1 - a) * (1 - b) ≤ 1 := by sorry