isExtr

Mathlib.Order.Filter.Extr

URI: https://scilib.ai/kg/mathlib#IsMinFilter.isExtr

English

If a is a minimal element with respect to f along a filter l, then f generates an extremal-filter at a.

Русский

Если a является минимальным элементом для f вдоль фильтра l, то f порождает экстремальный фильтр в точке a.

LaTeX

$$$IsMinFilter\ f\ l\ a \to IsExtrFilter\ f\ l\ a$$$

Lean4

theorem isExtr : IsMinFilter f l a → IsExtrFilter f l a :=
  Or.inl

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

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

Разделы

Аффилиация

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