Icc_orderDual_def

Mathlib.Order.Interval.Finset.Defs

URI: https://scilib.ai/kg/mathlib#Finset.Icc_orderDual_def

English

The open down-interval below b is finite in a LocallyFiniteOrder with bottom.

Русский

Открытый нижний интервал до b конечен в локально конечном порядке с нижней границей.

LaTeX

$$$\forall b \in \alpha, \lvert \{ x \in \alpha \mid x < b \} \rvert < \infty$$$

Lean4

theorem Icc_orderDual_def (a b : αᵒᵈ) : Icc a b = (Icc (ofDual b) (ofDual a)).map toDual.toEmbedding :=
  map_refl.symm

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

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

Разделы

Аффилиация

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