isSkeleton — Mathlib

English

Every object in FintypeCat.Skeleton is determined up to isomorphism by its length.

Русский

Каждый объект в FintypeCat.Skeleton определён до изоморфизма по своей длине.

LaTeX

$$$\\forall X:\\text{Skeleton},\\; X \\cong \\mathrm{mk}(\\mathrm{len}(X))$$$

Lean4

/-- `Fintype.Skeleton` is a skeleton of `Fintype`. -/
theorem isSkeleton : IsSkeletonOf FintypeCat Skeleton Skeleton.incl
    where
  skel := Skeleton.is_skeletal
  eqv := by infer_instance

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