orderIsoShrink_apply

Mathlib.Order.Shrink

URI: https://scilib.ai/kg/mathlib#orderIsoShrink_apply

English

For every a in α, the order isomorphism evaluated at a equals the natural Shrink embedding: orderIsoShrink(α)(a) = equivShrink(α)(a).

Русский

Для каждого a ∈ α значение orderIsoShrink(α)(a) равно equivShrink(α)(a).

LaTeX

$$$(\operatorname{orderIsoShrink}(\alpha))(a) = (\operatorname{equivShrink}(\alpha))(a)$$$

Lean4

@[simp]
theorem orderIsoShrink_apply [Preorder α] (a : α) : orderIsoShrink α a = equivShrink α a :=
  rfl

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

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

Разделы

Аффилиация

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