ofLex_apply

Mathlib.Order.PiLex

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

English

The i-th component of the Lex-constructed object equals the i-th component of the original function.

Русский

Компонента i у Lex-представления равна i-й компоненте исходной функции.

LaTeX

$$$ ofLex(x)_i = x_i $$$

Lean4

@[simp]
theorem ofLex_apply (x : Lex (∀ i, β i)) (i : ι) : ofLex x i = x i :=
  rfl

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

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

Разделы

Аффилиация

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