English
Let f: αᵒᵈ → βᵒᵈ be a function and a ∈ WithBot αᵒᵈ. Then the dualized image under WithBot.map respects duals via: WithBot.ofDual (WithBot.map f a) = map (ofDual ∘ f ∘ toDual) (WithBot.ofDual a).
Русский
Пусть f: αᵒᵈ → βᵒᵈ, a ∈ WithBot αᵒᵈ. Тогда двойственное отображение удовлетворяет: WithBot.ofDual (WithBot.map f a) = map (ofDual ∘ f ∘ toDual) (WithBot.ofDual a).
LaTeX
$$$ \operatorname{ofDual}(\mathrm{WithBot.map}(f,a)) = \mathrm{map}\bigl( \operatorname{ofDual} \circ f \circ \operatorname{toDual} \bigr)\bigl( \operatorname{WithBot.ofDual}(a) \bigr). $$$
Lean4
theorem ofDual_map (f : αᵒᵈ → βᵒᵈ) (a : WithBot αᵒᵈ) :
WithBot.ofDual (WithBot.map f a) = map (ofDual ∘ f ∘ toDual) (WithBot.ofDual a) :=
rfl
