4 abril 2024 – Calculemus

Si u ⊆ v, entonces f⁻¹[u] ⊆ f⁻¹[v]

PorJosé A. Alonso 4 abril 20244 abril 2024

Demostrar con Lean4 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

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