Iio_orderDual_def — Mathlib

English

In the dual order, the open lower interval Iio a equals the image of Ioi (ofDual a) under the embedding toDual.

Русский

В двойственном порядке открытый нижний интервал Iio a равен образу Ioi (ofDual a) под вложением toDual.

LaTeX

$$$ Iio a = (Ioi (ofDual a)).map toDual.toEmbedding $$$

Lean4

theorem Iio_orderDual_def (a : αᵒᵈ) : Iio a = (Ioi (ofDual a)).map toDual.toEmbedding :=
  map_refl.symm

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