monovary_comm

Mathlib.Order.Monotone.Monovary

URI: https://scilib.ai/kg/mathlib#monovary_comm

English

Monovary is commutative in the sense that Monovary f g is equivalent to Monovary g f.

Русский

Monovary коммутирует: Monovary f g равно Monovary g f.

LaTeX

$$$$ \\text{Monovary}(f,g) \\iff \\text{Monovary}(g,f) $$$$

Lean4

theorem monovary_comm : Monovary f g ↔ Monovary g f :=
  ⟨Monovary.symm, Monovary.symm⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru