junio 2022 – Calculemus

Si f·f es biyectiva, entonces f es biyectiva

PorJosé A. Alonso 28 junio 202228 junio 2022

Demostrar que si f·f es biyectiva, entonces f es biyectiva.

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

import tactic
open function

variable {X: Type}

example
  (f : X → X)
  (Hff : bijective (f ∘ f))
  : bijective f :=
sorry

import tactic

open function

variable {X: Type}

example

(f : X → X)

(Hff : bijective (f ∘ f))

: bijective f :=

sorry

Si g·f es suprayectiva, entonces g es suprayectiva

PorJosé A. Alonso 27 junio 2022

Demostrar que si g·f es suprayectiva, entonces g es suprayectiva.

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

import tactic
open function

variables {X Y Z : Type}
variable  {f : X → Y}
variable  {g : Y → Z}

example
  (Hgf : surjective (g ∘ f))
  : surjective g :=
sorry

import tactic

open function

variables {X Y Z : Type}

variable {f : X → Y}

variable {g : Y → Z}

example

(Hgf : surjective (g ∘ f))

: surjective g :=

sorry

Si g·f es inyectiva, entonces f es inyectiva.

PorJosé A. Alonso 22 junio 202222 junio 2022

Demostrar que si g·f es inyectiva, entonces f es inyectiva.

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

import tactic
open function

variables {X Y Z : Type}
variable  {f : X → Y}
variable  {g : Y → Z}

example
  (Hgf : injective (g ∘ f))
  : injective f :=
sorry

import tactic

open function

variables {X Y Z : Type}

variable {f : X → Y}

variable {g : Y → Z}

example

(Hgf : injective (g ∘ f))

: injective f :=

sorry