enero 2024 – Página 3

En los órdenes parciales, a < b ↔ a ≤ b ∧ a ≠ b

PorJosé A. Alonso 3 enero 202431 diciembre 2023

Demostrar con Lean4 que en los órdenes parciales,
$a < b ↔ a ≤ b ∧ a ≠ b$

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

import Mathlib.Tactic

variable {α : Type _} [PartialOrder α]
variable (a b : α)

example : a < b ↔ a ≤ b ∧ a ≠ b :=
by sorry

import Mathlib.Tactic

variable {α : Type _} [PartialOrder α]

variable (a b : α)

example : a < b ↔ a ≤ b ∧ a ≠ b :=

by sorry

PorJosé A. Alonso 2 enero 202429 diciembre 2023

Demostrar con Lean4 que la función $x ↦ -x$ no es monótona creciente.

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

import Mathlib.Data.Real.Basic
import src.CNS_de_no_monotona

example : ¬Monotone fun x : ℝ ↦ -x :=
by sorry

import Mathlib.Data.Real.Basic

import src.CNS_de_no_monotona

example : ¬Monotone fun x : ℝ ↦ -x :=

by sorry

PorJosé A. Alonso 1 enero 202429 diciembre 2023

Demostrar con Lean4 que $f: ℝ → ℝ$ no es monótona syss $(∃x,y)[x ≤ y ∧ f(x) > f(y)]$ .

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

import Mathlib.Data.Real.Basic
variable {f : ℝ → ℝ}

example :
  ¬Monotone f ↔ ∃ x y, x ≤ y ∧ f x > f y :=
sorry

import Mathlib.Data.Real.Basic

variable {f : ℝ → ℝ}

example :

¬Monotone f ↔ ∃ x y, x ≤ y ∧ f x > f y :=

sorry