Theorem Function.exists_fixed_point_of_surjective

Modification history

2026-03-30 14:04
Mathlib/Logic/Function/Basic.lean
feat(Logic/Function): add Lawvere fixed-point theorem (#35239) …
Added Function.exists_fixed_point_of_surjectiveView on Github →