dual_left — Mathlib

English

If f and g are Monovary, then the left-dualized version of f is antivary with g: Antivary (toDual ∘ f) g.

Русский

Если f и g монофортны (Monovary), то левый двойственный образ f вместе с g образуют antivary: Antivary (toDual ∘ f) g.

LaTeX

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

Lean4

theorem dual_left : Monovary f g → Antivary (toDual ∘ f) g :=
  id

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