English
Let f be a function from a topological space to a preordered set. The predicate IsLocalExtrOn f s a holds exactly when a is either a local minimum or a local maximum of f on the set s at the point a.
Русский
Пусть f — функция из топологического пространства в упорядоченное множество. Переменная IsLocalExtrOn f s a истинна тогда, когда в точке a на множестве s существуют окрестности, в которых a является либо локальным минимумом, либо локальным максимумом функции f.
LaTeX
$$$IsLocalExtrOn(f,s,a)\;:=\;IsExtrFilter(f,\,\mathcal{N}_s(a),\,a)$$$
Lean4
/-- `IsLocalExtrOn f s a` means `IsLocalMinOn f s a ∨ IsLocalMaxOn f s a`. -/
def IsLocalExtrOn :=
IsExtrFilter f (𝓝[s] a) a
