leOnePart_anti

Mathlib.Algebra.Order.Group.PosPart

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

English

The map a ↦ a⁺ᵐ is antitone with respect to the order: if a ≤ b then a⁺ᵐ ≥ b⁺ᵐ.

Русский

Отображение a ↦ a⁺ᵐ антимонотно: если a ≤ b, то a⁺ᵐ ≥ b⁺ᵐ.

LaTeX

$$Antitone( a ↦ a^{+m} )$$

Lean4

@[to_additive]
theorem leOnePart_anti : Antitone (leOnePart : α → α) := fun _a _b hab ↦ sup_le_sup_right (inv_le_inv_iff.2 hab) _

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

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

Разделы

Аффилиация

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