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:
|
1 2 3 4 5 6 7 8 9 10 |
import tactic variables {α : Type*} variables r s t : set α example (rs : r ⊆ s) (st : s ⊆ t) : r ⊆ t := sorry |