ext

Mathlib.Data.Set.Basic

URI: https://scilib.ai/kg/mathlib#SetCoe.ext

English

If two elements a and b of a set s have the same underlying first component in α, then the two subtypes are equal.

Русский

Если два элемента a и b подтипа s имеют одинаковую проекцию в α, то эти элементы подтипа равны друг другу.

LaTeX

$$$(a : \alpha) = b \Rightarrow a = b$$$

Lean4

theorem ext {s : Set α} {a b : s} : (a : α) = b → a = b :=
  Subtype.eq

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

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

Разделы

Аффилиация

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