English
The fin operation restricts a finite set of natural numbers to those elements less than n and identifies them with Fin n, yielding a finite set of elements of Fin n.
Русский
Операция fin ограничивает конечное множество натуральных чисел элементами меньше n и идентифицирует их с Fin n, получая конечное множество элементов Fin n.
LaTeX
$$Fin n s := { ⟨m, hm⟩ : m ∈ s ∧ m < n }$$
Lean4
/-- Given a finset `s` of natural numbers and a bound `n`,
`s.fin n` is the finset of all elements of `s` less than `n`.
This definition was introduced to define a `LocallyFiniteOrder` instance on `Fin n`.
Later, this instance was rewritten using a more efficient `attachFin`.
Since this definition had no other uses in the library, it was deprecated.
-/
@[deprecated attachFin (since := "2025-04-08")]
protected def fin (n : ℕ) (s : Finset ℕ) : Finset (Fin n) :=
(s.subtype _).map Fin.equivSubtype.symm.toEmbedding
