instCanLiftFinsetToSetFinite — Mathlib

English

Finite sets can be lifted to finsets; there is a canonical way to regard a finite set as a finite set of elements.

Русский

Для конечных множеств существует каноническое отображение в Finset как множество элементов.

LaTeX

$$$$ \\text{There is a canonical lift } s \\mapsto s' \\text{ with } ↑s' = s \\text{ whenever } s \\text{ is finite.} $$$$

Lean4

/-- Finite sets can be lifted to finsets. -/
instance : CanLift (Set α) (Finset α) (↑) Set.Finite where prf _ hs := hs.exists_finset_coe

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