Ioo_coe_coe — Mathlib

English

The open interval (a, b) in WithBot α equals the image under Embedding.some of the open interval (a, b) in α: Ioo(a:WithBot α) b = (Ioo a b).map Embedding.some.

Русский

Открытый интервал (a, b) в WithBot α равен образу через Embedding.some открытого интервала (a, b) в α: Ioo(a:WithBot α) b = (Ioo a b).map Embedding.some.

LaTeX

$$$$ \\mathrm{Ioo}(a : \\mathrm{WithBot}\\ α) b = ( \\mathrm{Ioo} \\ a \\ b ).\\mathrm{map} \\mathrm{Embedding}.some. $$$$

Lean4

theorem Ioo_coe_coe : Ioo (a : WithBot α) b = (Ioo a b).map Embedding.some :=
  rfl

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