toColex_monotone

Mathlib.Order.PiLex

URI: https://scilib.ai/kg/mathlib#Pi.toColex_monotone

English

The map f: ∀ i, β_i → Colex is monotone with respect to the lexicographic-like order on the Pi-type under WellFoundedGT.

Русский

Отображение f: ∀ i, β_i → Colex монотонно относительно порядка на Pi-типе при WellFoundedGT.

LaTeX

$$$\\text{Monotone}(\\mathrm{toColex})$ under the given orders.$$

Lean4

theorem toColex_monotone : Monotone (@toColex (∀ i, β i)) :=
  toLex_monotone (ι := ιᵒᵈ)

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

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

Разделы

Аффилиация

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