map_toDual

Mathlib.Order.WithBot

URI: https://scilib.ai/kg/mathlib#WithBot.map_toDual

English

For any f: αᵒᵈ → βᵒᵈ and a ∈ WithTop α, map f on the dual side equals map of a composed with dual.

Русский

Для f: αᵒᵈ → βᵒᵈ и a ∈ WithTop α: WithBot.map f (WithTop.toDual a) = a.map (toDual ∘ f).

LaTeX

$$$\\mathrm{WithBot}.map f (\\mathrm{WithTop}.toDual a) = a.map (toDual \\circ f)$$$

Lean4

theorem map_toDual (f : αᵒᵈ → βᵒᵈ) (a : WithTop α) : WithBot.map f (WithTop.toDual a) = a.map (toDual ∘ f) :=
  rfl

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

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

Разделы

Аффилиация

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