Ioo_bot_coe — Mathlib

English

In the WithBot extension, the interval (⊥, b) in α of α corresponds to Iio b mapped via Embedding.some: Ioo(⊥:WithBot α) b = (Iio b).map Embedding.some.

Русский

В расширении WithBot интервал (⊥, b) в α эквивалентен отображению Iio b через Embedding.some: Ioo(⊥:WithBot α) b = (Iio b).map Embedding.some.

LaTeX

$$$$ \\mathrm{Ioo}(\\perp, b) = ( \\mathrm{Iio}\\, b ).\\mathrm{map} \\mathrm{Embedding}.some. $$$$

Lean4

theorem Ioo_bot_coe : Ioo (⊥ : WithBot α) b = (Iio b).map Embedding.some :=
  rfl

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