13 noviembre 2023 – Calculemus

Si f: ℝ → ℝ es suprayectiva, entonces ∃x ∈ ℝ tal que f(x)² = 9

PorJosé A. Alonso 13 noviembre 20232 noviembre 2023

Demostrar con Lean4 que si $f: ℝ → ℝ$ es suprayectiva, entonces $∃x ∈ ℝ$ tal que $f(x)² = 9$ .

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Data.Real.Basic
open Function

example
  {f : ℝ → ℝ}
  (h : Surjective f)
  : ∃ x, (f x)^2 = 9 :=
by sorry

import Mathlib.Data.Real.Basic

open Function

example

{f : ℝ → ℝ}

(h : Surjective f)

: ∃ x, (f x)^2 = 9 :=

by sorry