unop — Mathlib

English

If a, x, y ∈ αᵐᵒᵖ satisfy SemiconjBy a x y, then SemiconjBy (unop a) (unop y) (unop x) holds.

Русский

Если для элементов a, x, y ∈ αᵐᵒᵖ выполняется SemiconjBy a x y, то SemiconjBy (unop a) (unop y) (unop x) тоже верно.

LaTeX

$$$\\SemiconjBy\\ (\\operatorname{unop} a)\\ (\\operatorname{unop} y)\\ (\\operatorname{unop} x)\\ \\,\\leftarrow\\,\\SemiconjBy\\ a\\ x\\ y$$$

Lean4

@[to_additive]
theorem _root_.SemiconjBy.unop [Mul α] {a x y : αᵐᵒᵖ} (h : SemiconjBy a x y) : SemiconjBy (unop a) (unop y) (unop x) :=
  semiconjBy_unop.2 h

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