dual — Mathlib

English

If f and g are Monovary, then their dual-order versions are Monovary: Monovary(f, g) ⇒ Monovary(toDual ∘ f, toDual ∘ g).

Русский

Если f и g удовлетворяют Monovary, то их варианты в дуальном порядке тоже удовлетворяют Monovary.

LaTeX

$$$\\operatorname{Monovary}(f,g) \\Rightarrow \\operatorname{Monovary}(\\operatorname{toDual} \\circ f, \\operatorname{toDual} \\circ g)$$$

Lean4

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

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