monotone_sort

Mathlib.Data.Fin.Tuple.Sort

URI: https://scilib.ai/kg/mathlib#Tuple.monotone_sort

English

The composition f ∘ sort f is monotone.

Русский

Отображение f ∘ sort f монотонно.

LaTeX

$$$\\mathrm{Monotone}(f \\circ \\mathrm{sort}(f)).$$$

Lean4

theorem monotone_sort (f : Fin n → α) : Monotone (f ∘ sort f) :=
  by
  rw [self_comp_sort]
  exact (monotone_proj f).comp (graphEquiv₂ f).monotone

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

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

Разделы

Аффилиация

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