map_neBot_iff

Mathlib.Order.Filter.Map

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

English

The nonemptiness of a mapped filter is equivalent to the nonemptiness of the original filter.

Русский

Неопустость отображенного фильтра эквивалентна неопустости исходного фильтра.

LaTeX

$$NeBot (map m F) ↔ NeBot F$$

Lean4

theorem map_neBot_iff (f : α → β) {F : Filter α} : NeBot (map f F) ↔ NeBot F := by
  simp only [neBot_iff, Ne, map_eq_bot_iff]

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

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

Разделы

Аффилиация

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