ext

Mathlib.CategoryTheory.FintypeCat

URI: https://scilib.ai/kg/mathlib#FintypeCat.Skeleton.ext

English

Two skeleton objects are equal if their lengths agree.

Русский

Два объекта скелета равны тогда и только тогда, когда их длины совпадают.

LaTeX

$$$\\forall X,Y: \\text{Skeleton},\\; \\mathrm{len}(X) = \\mathrm{len}(Y) \\Rightarrow X = Y$$$

Lean4

@[ext]
theorem ext (X Y : Skeleton) : X.len = Y.len → X = Y :=
  ULift.ext _ _

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

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

Разделы

Аффилиация

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