smul_filter

Mathlib.Order.Filter.Pointwise

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

English

f.NeBot → (a • f).NeBot.

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem smul_filter : f.NeBot → (a • f).NeBot := fun h => h.map _

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

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

Разделы

Аффилиация

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