mk_lt_mk_iff

Mathlib.Data.Sigma.Order

URI: https://scilib.ai/kg/mathlib#Sigma.mk_lt_mk_iff

← MathLib Explorer

English

For all indices i, and a,b ∈ αi, (⟨i,a⟩) < ⟨i,b⟩ iff a < b, given LT on each αi.

Русский

Для каждого i и a,b∈αi: (⟨i,a⟩) < ⟨i,b⟩ эквивалентно a < b.

LaTeX

$$$(\\langle i,a\\rangle < \\langle i,b\\rangle) \\iff a < b.$$$

Lean4

@[simp]
theorem mk_lt_mk_iff [∀ i, LT (α i)] {i : ι} {a b : α i} : (⟨i, a⟩ : Sigma α) < ⟨i, b⟩ ↔ a < b :=
  ⟨fun ⟨_, _, _, h⟩ => h, Sigma.LT.fiber _ _ _⟩

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

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

Разделы

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

Аффилиация

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