DAO: La semana en Calculemus (27 de noviembre de 2022)

import tactic
 
variables {α : Type*} [partial_order α]
variables s : set α
variables a b : α
 
-- (cota_superior s a) expresa que a es una cota superior de s.
def cota_superior (s : set α) (a : α) := ∀ {x}, x ∈ s → x ≤ a
 
example
  (h1 : cota_superior s a)
  (h2 : a ≤ b)
  : cota_superior s b :=
sorry

import tactic
 
variables {α : Type*} [partial_order α]
variables s : set α
variables a b : α
 
-- (cota_superior s a) expresa que a es una cota superior de s.
def cota_superior (s : set α) (a : α) := ∀ {x}, x ∈ s → x ≤ a
 
-- 1ª demostración
-- ===============
 
example
  (h1 : cota_superior s a)
  (h2 : a ≤ b)
  : cota_superior s b :=
begin
  intro x,
  assume xs : x ∈ s,
  have h3 : x ≤ a := h1 xs,
  show x ≤ b,
    by exact le_trans h3 h2,
end
 
-- 2ª demostración
-- ===============
 
example
  (h1 : cota_superior s a)
  (h2 : a ≤ b)
  : cota_superior s b :=
begin
  intros x xs,
  calc x ≤ a : h1 xs
     ... ≤ b : h2
end

import data.real.basic
 
open function
 
variable {c : ℝ}
 
example : injective (λ x, x + c) :=
sorry

import data.real.basic
 
open function
variable {c : ℝ}
 
-- 1ª demostración
-- ===============
 
example : injective (λ x, x + c) :=
begin
  assume x1 : ℝ,
  assume x2 : ℝ,
  assume h1 : (λ x, x + c) x1 = (λ x, x + c) x2,
  have h2 : x1 + c = x2 + c := h1,
  show x1 = x2,
    by exact (add_left_inj c).mp h2,
end
 
-- 2ª demostración
-- ===============
 
example : injective (λ x, x + c) :=
begin
  intros x1 x2 h,
  change x1 + c = x2 + c at h,
  apply add_right_cancel h,
end
 
-- 3ª demostración
-- ===============
 
example : injective (λ x, x + c) :=
begin
  intros x1 x2 h,
  apply (add_left_inj c).mp,
  exact h,
end
 
-- 4ª demostración
-- ===============
 
example : injective (λ x, x + c) :=
λ x1 x2 h, (add_left_inj c).mp h

import data.real.basic
 
open function
 
variable {c : ℝ}
 
example
  (h : c ≠ 0)
  : injective (λ x, c * x) :=
sorry

import data.real.basic
 
open function
 
variable {c : ℝ}
 
-- 1ª demostración
-- ===============
 
example
  (h : c ≠ 0)
  : injective (λ x, c * x) :=
begin
  assume x1 : ℝ,
  assume x2 : ℝ,
  assume h1 : (λ x, c * x) x1 = (λ x, c * x) x2,
  have h2 : c * x1 = c * x2 := h1,
  show x1 = x2,
    by exact (mul_right_inj' h).mp h1,
end
 
-- 2ª demostración
-- ===============
 
example
  (h : c ≠ 0)
  : injective (λ x, c * x) :=
begin
  intros x1 x2 h',
  dsimp at h',
  apply mul_left_cancel₀ h,
  exact h',
end
 
-- 3ª demostración
-- ===============
 
example
  (h : c ≠ 0)
  : injective (λ x, c * x) :=
begin
  intros x1 x2 h',
  dsimp at h',
  exact (mul_right_inj' h).mp h'
end
 
-- 3ª demostración
-- ===============
 
example
  {c : ℝ}
  (h : c ≠ 0)
  : injective (λ x, c * x) :=
λ x1 x2 h', mul_left_cancel₀ h h'

import tactic
 
open function
 
variables {A : Type*} {B : Type*} {C : Type*}
variables {f : A → B} {g : B → C}
 
example
  (hg : injective g)
  (hf : injective f) :
  injective (g ∘ f) :=
sorry

import tactic
 
open function
 
variables {A : Type*} {B : Type*} {C : Type*}
variables {f : A → B} {g : B → C}
 
-- 1ª demostración
-- ===============
 
example
  (hg : injective g)
  (hf : injective f) :
  injective (g ∘ f) :=
begin
  assume x : A,
  assume y : A,
  assume h1: (g ∘ f) x = (g ∘ f) y,
  have h2: g (f x) = g (f y) := h1,
  have h3: f x = f y := hg h2,
  show x = y,
    by exact hf h3,
end
 
-- 2ª demostración
-- ===============
 
example
  (hg : injective g)
  (hf : injective f) :
  injective (g ∘ f) :=
begin
  intros x y h,
  apply hf,
  apply hg,
  apply h,
end
 
-- 3ª demostración
-- ===============
 
example
  (hg : injective g)
  (hf : injective f) :
  injective (g ∘ f) :=
λ x y h, hf (hg h)
 
-- 4ª demostración
-- ===============
 
example
  (hg : injective g)
  (hf : injective f) :
  injective (g ∘ f) :=
-- by library_search
injective.comp hg hf
 
-- 5ª demostración
-- ===============
 
example
  (hg : injective g)
  (hf : injective f) :
  injective (g ∘ f) :=
-- by hint
by tauto

import data.real.basic
 
example : ∃ x : ℝ, 2 < x ∧ x < 3 :=
sorry

import data.real.basic
 
-- 1ª demostración
-- ===============
 
example : ∃ x : ℝ, 2 < x ∧ x < 3 :=
begin
  have h : 2 < (5 : ℝ) / 2 ∧ (5 : ℝ) / 2 < 3,
    by norm_num,
  show ∃ x : ℝ, 2 < x ∧ x < 3,
    by exact Exists.intro (5 / 2) h,
end
 
-- 2ª demostración
-- ===============
 
example : ∃ x : ℝ, 2 < x ∧ x < 3 :=
begin
  have h : 2 < (5 : ℝ) / 2 ∧ (5 : ℝ) / 2 < 3,
    by norm_num,
  show ∃ x : ℝ, 2 < x ∧ x < 3,
    by exact ⟨5 / 2, h⟩,
end
 
-- 3ª demostración
-- ===============
 
example : ∃ x : ℝ, 2 < x ∧ x < 3 :=
begin
  use 5 / 2,
  norm_num
end
 
-- 4ª demostración
-- ===============
 
example : ∃ x : ℝ, 2 < x ∧ x < 3 :=
⟨5 / 2, by norm_num⟩