closure — Mathlib

English

If a function is locally externally monotone on a set at a, then its closure preserves this local external monotonicity.

Русский

Если функция локально экстренно монотонна на множестве в точке a, то продолжение сохраняет локальную экстронную монотонность.

LaTeX

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

Lean4

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

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