Menu Close

Día: 19 noviembre 2022

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

Demostrar que si r ⊆ s y s ⊆ t, entonces r ⊆ t.

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

import tactic
 
variables {α : Type*}
variables r s t : set α
 
example
  (rs : r ⊆ s)
  (st : s ⊆ t)
  : r ⊆ t :=
sorry