equivShrink_bot

Mathlib.Order.Shrink

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

English

If α has a bottom element, bottom is preserved by equivShrink: equivShrink(α)(⊥) = ⊥.

Русский

Если у α есть нижняя граница, то нижняя граница сохраняется через equivShrink: equivShrink(α)(⊥) = ⊥.

LaTeX

$$$\operatorname{equivShrink}(\alpha)(\bot) = \bot$$$

Lean4

@[simp]
theorem equivShrink_bot [Bot α] : equivShrink.{u} α ⊥ = ⊥ :=
  rfl

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

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

Разделы

Аффилиация

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