uIoo_toDual — Mathlib

English

In the order dual, the unordered open interval corresponds to the preimage of the original interval under the order-reversing isomorphism.

Русский

В порядке двойственности неупорядоченный открытый интервал соответствует обратнообразованию исходного интервала под отображением, обращающим порядок.

LaTeX

$$$ uIoo( toDual(a), toDual(b) ) = (toDual)^{-1}\bigl( uIoo(a,b) \bigr) $$$

Lean4

@[simp]
theorem uIoo_toDual (a b : α) : uIoo (toDual a) (toDual b) = ofDual ⁻¹' uIoo a b :=
  Ioo_toDual (α := α)

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