map_neBot

Mathlib.Order.Filter.Map

URI: https://scilib.ai/kg/mathlib#Filter.map_neBot

English

If a filter F is nontrivial, then its image under m is nontrivial.

Русский

Если фильтр F непустой, то образ через m непустой.

LaTeX

$$NeBot f ⇒ NeBot (map m f)$$

Lean4

instance map_neBot [hf : NeBot f] : NeBot (f.map m) :=
  hf.map m

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

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

Разделы

Аффилиация

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