Finsets in Fin n
#
A few constructions for Finsets in Fin n
.
Main declarations #
Finset.attachFin
: Turns a Finset of naturals strictly less thann
into aFinset (Fin n)
.
@[simp]
@[deprecated Finset.attachFin (since := "2025-04-08")]
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.
Equations
- Finset.fin n s = Finset.map Fin.equivSubtype.symm.toEmbedding (Finset.subtype (fun (i : ℕ) => i < n) s)
Instances For
@[simp, deprecated Finset.mem_attachFin (since := "2025-04-08")]
@[simp, deprecated Finset.coe_attachFin (since := "2025-04-08")]
@[deprecated Finset.attachFin_subset_attachFin (since := "2025-04-08")]
@[deprecated Finset.attachFin_subset_attachFin (since := "2025-04-08")]
@[simp, deprecated Finset.map_valEmbedding_attachFin (since := "2025-04-08")]
@[deprecated "No replacement" (since := "2025-04-08")]