José A. AlonsoDemostrar 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 |
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 |