16 abril 2024 – Calculemus

f[s] \ f[t] ⊆ f[s \ t]

PorJosé A. Alonso 16 abril 2024

Demostrar con Lean4 que
\[f[s] \setminus f[t] ⊆ f[s \setminus t] \]

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

import Mathlib.Data.Set.Function
import Mathlib.Tactic

open Set

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

example : f '' s \ f '' t ⊆ f '' (s \ t) :=
by sorry

import Mathlib.Data.Set.Function

import Mathlib.Tactic

open Set

variable {α β : Type _}

variable (f : α → β)

variable (s t : Set α)

example : f '' s \ f '' t ⊆ f '' (s \ t) :=

by sorry