English
Let f: α → β be any function and a ∈ WithBot α. Then the dual of the image of a under the bottom-addition map is obtained by applying the bottom-compat map to the dual of a: toDual(WithBot.map f a) = map (toDual ∘ f ∘ ofDual) (toDual a).
Русский
Пусть f: α → β произвольна, и a ∈ WithBot α. Тогда двойственность сохраняет отображение: toDual(WithBot.map f a) = map (toDual ∘ f ∘ ofDual) (toDual a).
LaTeX
$$$ \operatorname{toDual}(\mathrm{WithBot.map}(f,a)) = \mathrm{map}\Bigl( \operatorname{toDual} \circ f \circ \operatorname{ofDual} \Bigr)\bigl( \operatorname{toDual}(a) \bigr). $$$$
Lean4
theorem toDual_map (f : α → β) (a : WithBot α) :
WithBot.toDual (WithBot.map f a) = map (toDual ∘ f ∘ ofDual) (WithBot.toDual a) :=
rfl
