Ioc_coe_coe — Mathlib

English

The interval (a, b] in WithBot α corresponds to (Ioc a b) mapped via Embedding.some into WithBot α: Ioc(a:WithBot α) b = (Ioc a b).map Embedding.some.

Русский

Интервал (a, b] в WithBot α соответствует (Ioc a b), отображённому через Embedding.some в WithBot α: Ioc(a:WithBot α) b = (Ioc a b).map Embedding.some.

LaTeX

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

Lean4

theorem Ioc_coe_coe : Ioc (a : WithBot α) b = (Ioc a b).map Embedding.some :=
  rfl

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