Si `f x ≤ f y → x ≤ y`, entonces f es inyectiva

Sea f una función de ℝ en ℝ tal que

   ∀ x y, f(x) ≤ f(y) → x ≤ y

1	∀ x y, f(x) ≤ f(y) → x ≤ y

Demostrar que f es inyectiva.

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

import data.real.basic
open function

variable (f : ℝ → ℝ)

example
  (h : ∀ {x y}, f x ≤ f y → x ≤ y)
  : injective f :=
sorry

import data.real.basic

open function

variable (f : ℝ → ℝ)

example

(h : ∀ {x y}, f x ≤ f y → x ≤ y)

: injective f :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic
open function

variable (f : ℝ → ℝ)

-- 1ª demostración
example
  (h : ∀ {x y}, f x ≤ f y → x ≤ y)
  : injective f :=
begin
  intros x y hxy,
  apply le_antisymm,
  { apply h,
    exact le_of_eq hxy, },
  { apply h,
    exact ge_of_eq hxy, },
end

-- 2ª demostración
example
  (h : ∀ {x y}, f x ≤ f y → x ≤ y)
  : injective f :=
begin
  intros x y hxy,
  apply le_antisymm,
  { exact h (le_of_eq hxy), },
  { exact h (ge_of_eq hxy), },
end

-- 3ª demostración
example
  (h : ∀ {x y}, f x ≤ f y → x ≤ y)
  : injective f :=
λ x y hxy, le_antisymm (h hxy.le) (h hxy.ge)

import data.real.basic

open function

variable (f : ℝ → ℝ)

-- 1ª demostración

example

(h : ∀ {x y}, f x ≤ f y → x ≤ y)

: injective f :=

begin

intros x y hxy,

apply le_antisymm,

{ apply h,

exact le_of_eq hxy, },

{ apply h,

exact ge_of_eq hxy, },

end

-- 2ª demostración

example

(h : ∀ {x y}, f x ≤ f y → x ≤ y)

: injective f :=

begin

intros x y hxy,

apply le_antisymm,

{ exact h (le_of_eq hxy), },

{ exact h (ge_of_eq hxy), },

end

-- 3ª demostración

example

(h : ∀ {x y}, f x ≤ f y → x ≤ y)

: injective f :=

λ x y hxy, le_antisymm (h hxy.le) (h hxy.ge)

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory "Si_f(x)_leq_f(y)_to_x_leq_y,_entonces_f_es_inyectiva"
imports Main HOL.Real
begin

(* 1ª demostración *)
lemma
  fixes f :: "real ⇒ real"
  assumes "∀ x y. f x ≤ f y ⟶ x ≤ y"
  shows   "inj f"
proof (rule injI)
  fix x y
  assume "f x = f y"
  show "x = y"
  proof (rule antisym)
    show "x ≤ y" 
      by (simp only: assms ‹f x = f y›)
  next
    show "y ≤ x"
      by (simp only: assms ‹f x = f y›)
  qed
qed

(* 2ª demostración *)
lemma
  fixes f :: "real ⇒ real"
  assumes "∀ x y. f x ≤ f y ⟶ x ≤ y"
  shows   "inj f"
proof (rule injI)
  fix x y
  assume "f x = f y"
  then show "x = y"
    using assms
    by (simp add: eq_iff)
qed

(* 3ª demostración *)
lemma
  fixes f :: "real ⇒ real"
  assumes "∀ x y. f x ≤ f y ⟶ x ≤ y"
  shows   "inj f"
  by (smt (verit, ccfv_threshold) assms inj_on_def)

end

theory "Si_f(x)_leq_f(y)_to_x_leq_y,_entonces_f_es_inyectiva"

imports Main HOL.Real

begin

(* 1ª demostración *)

lemma

fixes f :: "real ⇒ real"

assumes "∀ x y. f x ≤ f y ⟶ x ≤ y"

shows "inj f"

proof (rule injI)

fix x y

assume "f x = f y"

show "x = y"

proof (rule antisym)

show "x ≤ y"

by (simp only: assms ‹f x = f y›)

show "y ≤ x"

by (simp only: assms ‹f x = f y›)

qed

(* 2ª demostración *)

lemma

fixes f :: "real ⇒ real"

assumes "∀ x y. f x ≤ f y ⟶ x ≤ y"

shows "inj f"

proof (rule injI)

fix x y

assume "f x = f y"

then show "x = y"

using assms

by (simp add: eq_iff)

qed

(* 3ª demostración *)

lemma

fixes f :: "real ⇒ real"

assumes "∀ x y. f x ≤ f y ⟶ x ≤ y"

shows "inj f"

by (smt (verit, ccfv_threshold) assms inj_on_def)

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Share this:

Escribe un comentarioCancel reply