Ioc_bot_coe — Mathlib

English

In the same framework, the interval (⊥, b] in WithBot α equals the image of the α-interval Iic b under Embedding.some. In symbols, Ioc(⊥:WithBot α) b = (Iic b).map Embedding.some.

Русский

В той же постановке, интервал (⊥, b] в WithBot α равен образу ∙ интервала Iic b из α через Embedding.some. То есть Ioc(⊥:WithBot α) b = (Iic b).map Embedding.some.

LaTeX

$$$$ \\mathrm{Ioc}(\\perp, b) = \\bigl( \\mathrm{Iic}\\, b \\bigr).\\mathrm{map}\\, \\mathrm{Embedding}.some. $$$$

Lean4

theorem Ioc_bot_coe : Ioc (⊥ : WithBot α) b = (Iic b).map Embedding.some :=
  rfl

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