2 abril 2024 – Calculemus

Si f es suprayectiva, entonces u ⊆ f[f⁻¹[u]]

PorJosé A. Alonso 2 abril 20242 abril 2024

Demostrar con Lean4 que si \(f\) es suprayectiva, entonces
\[ u ⊆ f[f⁻¹[u]] \]

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

import Mathlib.Data.Set.Function
open Set Function
variable {α β : Type _}
variable (f : α → β)
variable (u : Set β)

example
  (h : Surjective f)
  : u ⊆ f '' (f⁻¹' u) :=
by sorry

import Mathlib.Data.Set.Function

open Set Function

variable {α β : Type _}

variable (f : α → β)

variable (u : Set β)

example

(h : Surjective f)

: u ⊆ f '' (f⁻¹' u) :=

by sorry