closure — Mathlib

English

If a function is externally monotone on a set at a, then it remains externally monotone on the closure.

Русский

Если функция экстренно монотонна на множестве в точке a, то она сохраняет это свойство на замыкании.

LaTeX

$$IsExtrOn f s a → ContinuousOn f (closure s) → IsExtrOn f (closure s) a.$$

Lean4

protected theorem closure (h : IsExtrOn f s a) (hc : ContinuousOn f (closure s)) : IsExtrOn f (closure s) a :=
  h.elim (fun h => Or.inl <| h.closure hc) fun h => Or.inr <| h.closure hc

Похожие утверждения