Si g·f es suprayectiva, entonces g es suprayectiva

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

Soluciones con Lean

import tactic
open function

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

-- 1ª demostración
example
  (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
  (Hgf : surjective (g ∘ f))
  : surjective g  := 
begin
  assume z : Z,
  rcases Hgf z with ⟨x : X, hx : (g ∘ f) x = z⟩,
  let y : Y := f x,
  use y,
  show g y = z, from
    calc g y = g (f x)   : rfl
         ... = (g ∘ f) x : rfl
         ... = z         : hx,
end

import tactic

open function

variables {X Y Z : Type}

variable {f : X → Y}

variable {g : Y → Z}

-- 1ª demostración

example

(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

(Hgf : surjective (g ∘ f))

: surjective g :=

begin

assume z : Z,

rcases Hgf z with ⟨x : X, hx : (g ∘ f) x = z⟩,

let y : Y := f x,

use y,

show g y = z, from

calc g y = g (f x) : rfl

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

... = z : hx,

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_gf_es_suprayectiva_entonces_g_es_suprayectiva
imports Main
begin 

lemma
  fixes   f :: "'a ⇒ 'b" and 
          g :: "'b ⇒ 'c"
  assumes "surj (g ∘ f)"
  shows   "surj g"
using assms by fastforce

end

theory Si_gf_es_suprayectiva_entonces_g_es_suprayectiva

imports Main

begin

lemma

fixes f :: "'a ⇒ 'b" and

g :: "'b ⇒ 'c"

assumes "surj (g ∘ f)"

shows "surj g"

using assms by fastforce

end

Share this:

Escribe un comentarioCancel reply