some_injective

Mathlib.Data.Option.Basic

URI: https://scilib.ai/kg/mathlib#Option.some_injective

English

The map a ↦ some a is injective.

Русский

Отображение a ↦ some a инъективно.

LaTeX

$$$$ \forall a,b, \mathrm{some}(a) = \mathrm{some}(b) \Rightarrow a = b. $$$$

Lean4

theorem some_injective (α : Type*) : Function.Injective (@some α) := fun _ _ ↦ some_inj.mp

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

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

Разделы

Аффилиация

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