Theorem Function.isConstOn_iff_exists_forall_eq_of_nonempty

Modification history

2026-11-11 01:06
Mathlib/Logic/Function/Const.lean
feat(Logic/Function): define `Function.IsConstOn` predicate (#45867) …
Added Function.isConstOn_iff_exists_forall_eq_of_nonemptyView on Github →