ofDual_map — Mathlib

English

The dual of a mapped dual respects dual maps: ofDual(map f a) equals the dual map composition applied to ofDual a.

Русский

Дуальное отображение соответствия сохраняется: ofDual(map f a) = map(ofDual ∘ f ∘ toDual)(ofDual a).

LaTeX

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

Lean4

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

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