map_toDual — Mathlib

English

Map respects duality: the dual of a mapped element corresponds to mapping under duals inside the dualized structure.

Русский

Отображение сохраняет дуальность: дуальное образ отображения соответствует отображению двойственной структуры.

LaTeX

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

Lean4

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

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