Commit 2026-03-30 14:04 349bfab4

feat(Logic/Function): add Lawvere fixed-point theorem (#35239) Adds Lawvere's fixed-point theorem. This is the classical diagonal argument that generalizes \cantor_surjective\ and \cantor_injective\ (both already in Mathlib). The proof is a two-line term-mode construction.