toDual_sInf

Mathlib.Order.CompleteLattice.Defs

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

English

Similarly, the dual of the infimum equals the supremum of the preimage under the duality map.

Русский

Аналогично, дуал нижней границы равен верхней границе изображения под дуальным отображением.

LaTeX

$$$\mathrm{toDual}(\sInf s) = \sSup (\mathrm{ofDual}^{-1} \; s)$$$

Lean4

@[simp]
theorem toDual_sInf [InfSet α] (s : Set α) : toDual (sInf s) = sSup (ofDual ⁻¹' s) :=
  rfl

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

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

Разделы

Аффилиация

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