neg

Mathlib.Order.Filter.ZeroAndBoundedAtFilter

URI: https://scilib.ai/kg/mathlib#Filter.BoundedAtFilter.neg

English

If f is bounded along l, then −f is bounded along l.

Русский

Если f ограничена вдоль l, то −f ограничена вдоль l.

LaTeX

$$$\\mathrm{BoundedAtFilter}(l,f) \\Rightarrow \\mathrm{BoundedAtFilter}(l,-f)$$$

Lean4

theorem neg [SeminormedAddCommGroup β] {l : Filter α} {f : α → β} (hf : BoundedAtFilter l f) : BoundedAtFilter l (-f) :=
  hf.neg_left

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

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

Разделы

Аффилиация

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