localize

Mathlib.Topology.Order.LocalExtr

URI: https://scilib.ai/kg/mathlib#IsExtrOn.localize

English

From IsLocalExtrOn f s a one can derive either IsLocalMinOn f s a or IsLocalMaxOn f s a; the elimination principle.

Русский

Из IsLocalExtrOn f s a следует либо IsLocalMinOn f s a, либо IsLocalMaxOn f s a; принцип устранения.

LaTeX

$$$IsLocalExtrOn f s a \rightarrow (IsLocalMinOn f s a) \lor (IsLocalMaxOn f s a)$$$

Lean4

theorem localize (hf : IsExtrOn f s a) : IsLocalExtrOn f s a :=
  hf.filter_mono <| inf_le_right

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru