lean_workbook_plus_71767
ProvedThe function from is surjective
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_71767 : ∀ x : ℝ, x ∈ Set.Icc 0 1 → ∃ y : ℝ, y ∈ Set.Icc 0 1 ∧ y ^ 2 = x := by sorry
Source
The function from is surjective
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_71767 : ∀ x : ℝ, x ∈ Set.Icc 0 1 → ∃ y : ℝ, y ∈ Set.Icc 0 1 ∧ y ^ 2 = x := by sorry