Si f·f es biyectiva, entonces f es biyectiva

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

Soluciones con Lean

import tactic
open function

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

-- 1ª demostración
-- ===============

lemma iny_comp_iny_primera
  (Hgf : injective (g ∘ f))
  : injective f :=
begin
  intros x x' f_xx',
  apply Hgf,
  finish,
end

lemma supr_comp_supr_segunda
  (Hgf : surjective (g ∘ f))
  : surjective g :=
begin
  intros z,
  rcases Hgf z with ⟨x, hx⟩,
  use f x,
  calc g (f x) = (g ∘ f) x : rfl
           ... = z         : hx,
end

example
  (f : X → X)
  (Hff : bijective (f ∘ f))
  : bijective f :=
begin
  split,
  { have h1 : injective (f ∘ f) := bijective.injective Hff,
    exact iny_comp_iny_primera h1, },
  { have h2 : surjective (f ∘ f) := bijective.surjective Hff,
    exact supr_comp_supr_segunda h2, },
end

import tactic

open function

variables {X Y Z : Type}

variable {f : X → Y}

variable {g : Y → Z}

-- 1ª demostración

-- ===============

lemma iny_comp_iny_primera

(Hgf : injective (g ∘ f))

: injective f :=

begin

intros x x' f_xx',

apply Hgf,

finish,

end

lemma supr_comp_supr_segunda

(Hgf : surjective (g ∘ f))

: surjective g :=

begin

intros z,

rcases Hgf z with ⟨x, hx⟩,

use f x,

calc g (f x) = (g ∘ f) x : rfl

... = z : hx,

end

example

(f : X → X)

(Hff : bijective (f ∘ f))

: bijective f :=

begin

split,

{ have h1 : injective (f ∘ f) := bijective.injective Hff,

exact iny_comp_iny_primera h1, },

{ have h2 : surjective (f ∘ f) := bijective.surjective Hff,

exact supr_comp_supr_segunda h2, },

end

El código de las demostraciones se encuentra en GitHub y puede ejecutarse con el Lean Web editor.

Soluciones con Isabelle/HOL

theory Si_ff_es_biyectiva_entonces_f_es_biyectiva
imports Main
begin 

lemma
  assumes "bij (f ∘ f)"
  shows   "bij f"
proof (rule bijI)
  show "inj f" 
  proof -
    have h1 : "inj (f ∘ f)"
      using assms by (simp only: bij_is_inj)
    then show "inj f"
      by (simp only: inj_on_imageI2)
  qed 
next
  show "surj f"
  proof -
    have h2 : "surj (f ∘ f)"
      using assms by (simp only: bij_is_surj)
    then show "surj f"
      by auto
  qed
qed

end

theory Si_ff_es_biyectiva_entonces_f_es_biyectiva

imports Main

begin

lemma

assumes "bij (f ∘ f)"

shows "bij f"

proof (rule bijI)

show "inj f"

proof -

have h1 : "inj (f ∘ f)"

using assms by (simp only: bij_is_inj)

then show "inj f"

by (simp only: inj_on_imageI2)

qed

show "surj f"

proof -

have h2 : "surj (f ∘ f)"

using assms by (simp only: bij_is_surj)

then show "surj f"

by auto

qed

end

Share this:

Escribe un comentarioCancel reply