map_atBot

Mathlib.Order.Filter.AtTopBot.Map

URI: https://scilib.ai/kg/mathlib#OrderIso.map_atBot

English

If e is an order isomorphism, then pushing forward the filter atBot along e yields atBot: map e atBot = atBot.

Русский

Если e — порядок-изоморфизм, то отображение фильтра на дно сохраняется: map e atBot = atBot.

LaTeX

$$$\\operatorname{map}(e)\\operatorname{atBot} = \\operatorname{atBot}$$$

Lean4

@[simp]
theorem map_atBot (e : α ≃o β) : map (e : α → β) atBot = atBot :=
  e.dual.map_atTop

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

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

Разделы

Аффилиация

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