6 abril 2024 – Calculemus

f⁻¹[A ∪ B] = f⁻¹[A] ∪ f⁻¹[B]

PorJosé A. Alonso 6 abril 2024

Demostrar con Lean4 que \(f⁻¹[A ∪ B] = f⁻¹[A] ∪ f⁻¹[B]\).

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

import Mathlib.Data.Set.Function

open Set

variable {α β : Type _}
variable (f : α → β)
variable (A B : Set β)

example : f ⁻¹' (A ∪ B) = f ⁻¹' A ∪ f ⁻¹' B :=
by sorry

import Mathlib.Data.Set.Function

open Set

variable {α β : Type _}

variable (f : α → β)

variable (A B : Set β)

example : f ⁻¹' (A ∪ B) = f ⁻¹' A ∪ f ⁻¹' B :=

by sorry