rev_strictAnti

Mathlib.Order.Fin.Basic

URI: https://scilib.ai/kg/mathlib#Fin.rev_strictAnti

English

The reverse map is strictly antitone: rev is strictly anti-order-preserving.

Русский

Обратное отображение является строго антиупорядоченным: функция rev инвертирует порядок строго.

LaTeX

$$$\forall {n : \mathbb{N}}, \; \text{StrictAnti}(\mathrm{rev})$$$

Lean4

theorem rev_strictAnti : StrictAnti (@rev n) := fun _ _ ↦ rev_lt_rev.mpr

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

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

Разделы

Аффилиация

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