15 abril 2024 – Calculemus

Si f es inyectiva, entonces f[s] ∩ f[t] ⊆ f[s ∩ t]

PorJosé A. Alonso 15 abril 202415 abril 2024

Demostrar con Lean4 que si \(f\) es inyectiva, entonces
\[ f[s] ∩ f[t] ⊆ f[s ∩ t] \]

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

import Mathlib.Data.Set.Function

open Set Function

variable {α β : Type _}
variable (f : α → β)
variable (s t : Set α)

example
  (h : Injective f)
  : f '' s ∩ f '' t ⊆ f '' (s ∩ t) :=
by sorry

import Mathlib.Data.Set.Function

open Set Function

variable {α β : Type _}

variable (f : α → β)

variable (s t : Set α)

example

(h : Injective f)

: f '' s ∩ f '' t ⊆ f '' (s ∩ t) :=

by sorry