some_eq_iff

Mathlib.Topology.Compactification.OnePoint.Basic

URI: https://scilib.ai/kg/mathlib#OnePoint.some_eq_iff

English

The constructor Some is injective: Some x1 = Some x2 if and only if x1 = x2.

Русский

Конструктор Some инъективен: Some x1 = Some x2 тогда и только тогда, когда x1 = x2.

LaTeX

$$$(\\operatorname{Some} x_1 = \\operatorname{Some} x_2) \\iff x_1 = x_2$$$

Lean4

@[simp]
theorem some_eq_iff (x₁ x₂ : X) : (some x₁ = some x₂) ↔ (x₁ = x₂) :=
  by
  rw [iff_eq_eq]
  exact Option.some.injEq x₁ x₂

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

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

Разделы

Аффилиация

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