some_inj

Mathlib.Data.Part

URI: https://scilib.ai/kg/mathlib#Part.some_inj

English

For all a,b, (some a) = (some b) iff a = b.

Русский

Для всех a,b: some a = some b тогда и только тогда, когда a = b.

LaTeX

$$$$\forall a,b:\alpha,\; \mathrm{some}(a) = \mathrm{some}(b) \iff a = b.$$$$

Lean4

@[simp]
theorem some_inj {a b : α} : Part.some a = some b ↔ a = b :=
  some_injective.eq_iff

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

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

Разделы

Аффилиация

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