monotone_proj

Mathlib.Data.Fin.Tuple.Sort

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

← MathLib Explorer

English

The projection map from the graph to α is monotone.

Русский

Отображение проекции из графа на α монотонно.

LaTeX

$$$\\mathrm{Monotone}(\\mathrm{graph.proj})$$$

Lean4

theorem monotone_proj (f : Fin n → α) : Monotone (graph.proj : graph f → α) :=
  by
  rintro ⟨⟨x, i⟩, hx⟩ ⟨⟨y, j⟩, hy⟩ (_ | h)
  · exact le_of_lt ‹_›
  · simp [graph.proj]

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

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

Разделы

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

Аффилиация

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