22 abril 2024 – Calculemus

Unión con la imagen

PorJosé A. Alonso 22 abril 202422 abril 2024

Demostrar con Lean4 que
\[ f[s ∪ f⁻¹[v]] ⊆ f[s] ∪ v \]

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 : Set α)
variable (v : Set β)

example : f '' (s ∪ f ⁻¹' v) ⊆ f '' s ∪ v :=
by sorry

import Mathlib.Data.Set.Function

import Mathlib.Tactic

open Set

variable (α β : Type _)

variable (f : α → β)

variable (s : Set α)

variable (v : Set β)

example : f '' (s ∪ f ⁻¹' v) ⊆ f '' s ∪ v :=

by sorry