29 abril 2024 – Calculemus

Imagen de la interseccion general mediante aplicaciones inyectivas

PorJosé A. Alonso 29 abril 202430 abril 2024

Demostrar con Lean4 que si \(f\) es inyectiva, entonces
\[⋂ᵢf[Aᵢ] ⊆ f\left[⋂ᵢAᵢ\right] \]

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

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

open Set Function

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

example
  (i : I)
  (injf : Injective f)
  : (⋂ i, f '' A i) ⊆ f '' (⋂ i, A i) :=
by
sorry

import Mathlib.Data.Set.Basic

import Mathlib.Tactic

open Set Function

variable {α β I : Type _}

variable (f : α → β)

variable (A : I → Set α)

example

(i : I)

(injf : Injective f)

: (⋂ i, f '' A i) ⊆ f '' (⋂ i, A i) :=

sorry