inclusionBoolΓ'_injective

Mathlib.Computability.Encoding

URI: https://scilib.ai/kg/mathlib#Computability.inclusionBoolΓ'_injective

← MathLib Explorer

English

The inclusion map from Bool into Γ' is injective.

Русский

Включение Bool в Γ' инъективно.

LaTeX

$$$ \operatorname{Injective}(\\mathrm{inclusionBool\\prime}) $$$

Lean4

theorem inclusionBoolΓ'_injective : Function.Injective inclusionBoolΓ' :=
  Function.HasLeftInverse.injective ⟨_, (fun _ => sectionΓ'Bool_inclusionBoolΓ')⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru