Demostraciones de "s ∩ ⋃_i A_i = ⋃_i (A_i ∩ s)"
Demostrar con Lean4 y con Isabelle/HOL que \[ s ∩ ⋃_i A_i = ⋃_i (A_i ∩ s) \]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Set.Basic import Mathlib.Data.Set.Lattice import Mathlib.Tactic open Set variable {α : Type} variable (s : Set α) variable (A : ℕ → Set α) example : s ∩ (⋃ i, A i) = ⋃ i, (A i ∩ s) := by sorry
y la siguiente teoría de Isabelle/HOL:
theory Distributiva_de_la_interseccion_respecto_de_la_union_general imports Main begin lemma "s ∩ (⋃ i ∈ I. A i) = (⋃ i ∈ I. (A i ∩ s))" sorry end