of_smul_filter

Mathlib.Order.Filter.Pointwise

URI: https://scilib.ai/kg/mathlib#Filter.NeBot.of_smul_filter

English

(a • f).NeBot → f.NeBot

Русский

(a • f).Непустой → f.Непустой

LaTeX

$$$ (a \cdot f).NeBot \Rightarrow f.NeBot $$$

Lean4

@[to_additive]
theorem of_smul_filter : (a • f).NeBot → f.NeBot :=
  NeBot.of_map

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

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

Разделы

Аффилиация

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