30 abril 2024 – Calculemus

Imagen inversa de la unión general

PorJosé A. Alonso 30 abril 202430 abril 2024

Demostrar con Lean4 que
\[ f⁻¹\left[⋃ᵢ Bᵢ\right] = ⋃ᵢ f⁻¹[Bᵢ] \]

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Data.Set.Basic
import Mathlib.Tactic

open Set

variable {α β I : Type _}
variable (f : α → β)
variable (B : I → Set β)

example : f ⁻¹' (⋃ i, B i) = ⋃ i, f ⁻¹' (B i) :=
by sorry

import Mathlib.Data.Set.Basic

import Mathlib.Tactic

open Set

variable {α β I : Type _}

variable (f : α → β)

variable (B : I → Set β)

example : f ⁻¹' (⋃ i, B i) = ⋃ i, f ⁻¹' (B i) :=

by sorry