monovaryOn_inv_right

Mathlib.Algebra.Order.Monovary

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

← MathLib Explorer

English

MonovaryOn f with g^{-1} on s is equivalent to AntivaryOn f with g on s.

Русский

MonovaryOn f с g^{-1} на s эквивалентна AntivaryOn f с g на s.

LaTeX

$$$$\\operatorname{MonovaryOn}(f, g^{-1}, s) \\iff \\operatorname{AntivaryOn}(f, g, s).$$$$

Lean4

@[to_additive (attr := simp)]
theorem monovaryOn_inv_right : MonovaryOn f g⁻¹ s ↔ AntivaryOn f g s := by
  simpa [MonovaryOn, AntivaryOn] using forall₂_swap

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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