coe_eq_coe

Mathlib.Topology.Compactification.OnePoint.Basic

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

English

For x, y ∈ X, (x : OnePoint X) = (y : OnePoint X) iff x = y.

Русский

Для x, y ∈ X имеет место: (x : OnePoint X) = (y : OnePoint X) эквивалентно x = y.

LaTeX

$$$(x : \\mathrm{OnePoint} X) = (y : \\mathrm{OnePoint} X) \\iff x = y$$$

Lean4

@[norm_cast]
theorem coe_eq_coe {x y : X} : (x : OnePoint X) = y ↔ x = y :=
  coe_injective.eq_iff

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

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

Разделы

Аффилиация

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