Validación formal en Lean4 dunha obstrución funcional: ausencia de imaxe implica non‑biyectividade

Este traballo presenta a validación formal, realizada en Lean4 (Mathlib), dunha obstrución funcional básica: unha función non pode ser biyectiva se existe un elemento do codominio que non é imaxe de ningún elemento do dominio. A demostración formaliza a contradición entre a hipótese de exclusión e a sobrexectividade, empregando a definición estándar de biyectividade e o mecanismo de certificación do asistente de teoremas. Inclúese o teorema en Lean4, a proba verificada e o estado intermedio da demostración, co obxectivo de documentar de maneira rigorosa unha incompatibilidade estrutural elemental e ilustrar o uso de Lean4 como ferramenta de verificación matemática.