lt_of_forall_lt_of_lt

Mathlib.Data.DFinsupp.Lex

URI: https://scilib.ai/kg/mathlib#DFinsupp.lt_of_forall_lt_of_lt

← MathLib Explorer

English

Let a,b ∈ Lex(Π_i α_i) and i ∈ I. If for all j < i we have a_j = b_j and a_i < b_i, then a < b.

Русский

Пусть a,b ∈ Lex(Π_i α_i) и i ∈ I. Если для всех j < i имеется a_j = b_j и a_i < b_i, то a < b.

LaTeX

$$$$ \\forall a,b,i,\\ (\\forall j

Lean4

theorem lt_of_forall_lt_of_lt (a b : Lex (Π₀ i, α i)) (i : ι) :
    (∀ j < i, ofLex a j = ofLex b j) → ofLex a i < ofLex b i → a < b := fun h1 h2 ↦ ⟨i, h1, h2⟩

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

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

Разделы

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

Аффилиация

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