Monotonía de la imagen inversa
Demostrar con Lean4 y con Isabelle/HOL que si \(u ⊆ v\), entonces \(f⁻¹[u] ⊆ f⁻¹[v]\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Set.Function open Set variable {α β : Type _} variable (f : α → β) variable (u v : Set β) example (h : u ⊆ v) : f ⁻¹' u ⊆ f ⁻¹' v := by sorry
y la siguiente teoría de Isabelle/HOL:
theory Monotonia_de_la_imagen_inversa imports Main begin lemma assumes "u ⊆ v" shows "f -` u ⊆ f -` v" sorry end