En Lean, la imagen inversa de un conjunto s (de elementos de tipo por la función f (de tipo α → β) es el conjunto f ⁻¹' s de elementos x (de tipo α) tales que f x ∈ s.
Demostrar que f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 |
import data.set.basic open set variables {α : Type*} {β : Type*} variable f : α → β variables u v : set β example : f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v := sorry |
Demostrar que s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s)
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 11 12 |
import data.set.basic import data.set.lattice import tactic open set variable {α : Type} variable s : set α variable A : ℕ → set α example : s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s) := sorry |
Read More «Distributiva de la intersección respecto de la unión general»
Demostrar que s ∩ (s ∪ t) = s
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 |
import data.set.basic open set variable {α : Type} variables s t : set α example : s ∩ (s ∪ t) = s := sorry |
Demostrar que (s \ t) \ u ⊆ s \ (t ∪ u)
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 |
import data.set.basic open set variable {α : Type} variables s t u : set α example : (s \ t) \ u ⊆ s \ (t ∪ u) := sorry |
Demostrar que s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u).
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 |
import data.set.basic open set variable {α : Type} variables s t u : set α example : s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) := sorry |
Read More «Propiedad semidistributiva de la intersección sobre la unión»
Demostrar que la intersección es monótona por la izquierda; es decir, si s ⊆ t, entonces s ∩ u ⊆ t ∩ u.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 |
import data.set.basic open set variable {α : Type} variables s t u : set α example (h : s ⊆ t) : s ∩ u ⊆ t ∩ u := sorry |