11 marzo 2024 – Calculemus

s ∪ ⋂ i, A i = ⋂ i, (A i ∪ s)

PorJosé A. Alonso 11 marzo 20248 marzo 2024

Demostrar con Lean4 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.Tactic
open Set
variable {α : Type}
variable (s : Set α)
variable (A : ℕ → Set α)

example : s ∪ (⋂ i, A i) = ⋂ i, (A i ∪ s) :=
by sorry

import Mathlib.Data.Set.Basic

import Mathlib.Tactic

open Set

variable {α : Type}

variable (s : Set α)

variable (A : ℕ → Set α)

example : s ∪ (⋂ i, A i) = ⋂ i, (A i ∪ s) :=

by sorry