Ioo_orderDual_def — Mathlib

English

In the dual order αᵒᵈ, the Ioo interval is the image of Ioo under the dual embedding, with endpoints swapped.

Русский

Во втором порядке αᵒᵈ интервал Ioo равен изображению Ioo через двойственное вложение, концы поменяны местами.

LaTeX

$$$Ioo(a,b) = (Ioo(ofDual b)(ofDual a)).map toDual.toEmbedding$$$

Lean4

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

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