3 abril 2024 – Calculemus

Si s ⊆ t, entonces f[s] ⊆ f[t]

PorJosé A. Alonso 3 abril 20243 abril 2024

Demostrar con Lean4 que si \(s ⊆ t\), entonces \(f[s] ⊆ f[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
  (h : s ⊆ t)
  : f '' s ⊆ f '' t :=
by sorry

import Mathlib.Data.Set.Function

import Mathlib.Tactic

open Set

variable {α β : Type _}

variable (f : α → β)

variable (s t : Set α)

example

(h : s ⊆ t)

: f '' s ⊆ f '' t :=

by sorry