20 octubre 2023 – Calculemus

Si r ⊆ s y s ⊆ t, entonces r ⊆ t

PorJosé A. Alonso 20 octubre 202317 octubre 2023

Demostrar con Lean4 que si \(r ⊆ s\) y \(s ⊆ t\), entonces \(r ⊆ t\).

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

import Mathlib.Tactic

open Set

variable {α : Type _}
variable (r s t : Set α)

example
  (rs : r ⊆ s)
  (st : s ⊆ t)
  : r ⊆ t :=
by sorry

import Mathlib.Tactic

open Set

variable {α : Type _}

variable (r s t : Set α)

example

(rs : r ⊆ s)

(st : s ⊆ t)

: r ⊆ t :=

by sorry