Imagen de la unión
En Lean, la imagen de un conjunto s por una función f se representa por f '' s; es decir, f '' s = {y | ∃ x, x ∈ s ∧ f x = y}
Demostrar que f '' (s ∪ t) = f '' s ∪ f '' t
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 11 |
import data.set.basic import tactic open set variables {α : Type*} {β : Type*} variable f : α → β variables s t : set α example : f '' (s ∪ t) = f '' s ∪ f '' t := sorry |