dual — Mathlib

English

Let f: I → α and g: I → β with α, β preordered. If f and g form an antivary pair, then their dualized versions f̃ := toDual ∘ f and g̃ := toDual ∘ g form antivary as well.

Русский

Пусть f: I → α и g: I → β, где α и β — частично упорядоченные множества. Если f и g образуют пару antivary, то их двойственные образы f̃ := toDual ∘ f и g̃ := toDual ∘ g также образуют antivary.

LaTeX

$$$\operatorname{Antivary}(f,g) \implies \operatorname{Antivary}(\mathrm{toDual} \circ f, \mathrm{toDual} \circ g)$$$

Lean4

theorem dual : Antivary f g → Antivary (toDual ∘ f) (toDual ∘ g) :=
  swap

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