lean_workbook_plus_65859

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Show that $A = \{ x<1, y>1 \}$ is open in $\mathbb{R} \times \mathbb{R}$ (but not the metric space $\mathbb{R}^2$ ).

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_65859 : IsOpen {p : ℝ × ℝ | p.fst < 1 ∧ p.snd > 1}   :=  by sorry

Source