f⁻¹[u ∩ v] = f⁻¹[u] ∩ f⁻¹[v]
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 con Lean4 que
|
1 |
f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v |
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Data.Set.Function variable {α β : Type _} variable (f : α → β) variable (u v : Set β) open Set example : f ⁻¹' (u ∩ v) = f ⁻¹' u ∩ f ⁻¹' v := by sorry |