Commit 2026-11-11 01:06 c9f80237

View on Github →

feat(Logic/Function): define Function.IsConstOn predicate (#45867) Add a predicate for a function being constant on a set. Basically copy over everything from Function.IsConst. This helps us state various theorem mrore cleaner, for example LipschitzOnWith.zero_iff Partly done with AI assistance (and review) to copy over the API

Estimated changes

Modified Mathlib/Logic/Function/Const.lean

added theorem Function.IsConst.isConstOn

added theorem Function.IsConst.isConstOn_comp

added theorem Function.IsConstOn.anti

added theorem Function.IsConstOn.comp_left

added theorem Function.IsConstOn.comp_right

added theorem Function.IsConstOn.congr

added theorem Function.IsConstOn.injOn_iff

added theorem Function.IsConstOn.of_eqOn

added theorem Function.IsConstOn.of_forall_eq

added theorem Function.IsConstOn.of_subsingleton

added def Function.IsConstOn

added theorem Function.isConstOn_and_injOn_iff

added theorem Function.isConstOn_empty

added theorem Function.isConstOn_id_iff

added theorem Function.isConstOn_iff

added theorem Function.isConstOn_iff_exists_eqOn_const

added theorem Function.isConstOn_iff_exists_eqOn_const_of_nonempty

added theorem Function.isConstOn_iff_exists_forall_eq

added theorem Function.isConstOn_iff_exists_forall_eq_of_nonempty

added theorem Function.isConstOn_iff_isConst_comp_val

added theorem Function.isConstOn_singleton

added theorem Function.isConstOn_univ

added theorem Function.not_isConstOn_iff_exists_apply_ne

added theorem Function.not_isConstOn_of_apply_ne

added theorem Set.EqOn.isConstOn_iff

added theorem Set.InjOn.isConstOn_iff

added theorem Set.nontrivial_image_iff

added theorem Set.subsingleton_image_iff

Modified Mathlib/Order/Filter/EventuallyConst.lean

Modified Mathlib/Topology/LocallyConstant/Basic.lean