Documentation

Mathlib.Data.Finset.Fin

Finsets in Fin n #

A few constructions for Finsets in Fin n.

Main declarations #

def Finset.attachFin (s : Finset ) {n : } (h : ms, m < n) :

Given a Finset s of contained in {0,..., n-1}, the corresponding Finset in Fin n is s.attachFin h where h is a proof that all elements of s are less than n.

Equations
Instances For
    @[simp]
    theorem Finset.mem_attachFin {n : } {s : Finset } (h : ms, m < n) {a : Fin n} :
    a s.attachFin h a s
    @[simp]
    theorem Finset.coe_attachFin {n : } {s : Finset } (h : ms, m < n) :
    (s.attachFin h) = Fin.val ⁻¹' s
    @[simp]
    theorem Finset.card_attachFin {n : } (s : Finset ) (h : ms, m < n) :
    @[simp]
    theorem Finset.image_val_attachFin {n : } {s : Finset } (h : ms, m < n) :
    @[simp]
    theorem Finset.map_valEmbedding_attachFin {n : } {s : Finset } (h : ms, m < n) :
    @[simp]
    theorem Finset.attachFin_subset_attachFin_iff {n : } {s t : Finset } (hs : ms, m < n) (ht : mt, m < n) :
    s.attachFin hs t.attachFin ht s t
    theorem Finset.attachFin_subset_attachFin {n : } {s t : Finset } (hst : s t) (ht : mt, m < n) :
    @[simp]
    theorem Finset.attachFin_ssubset_attachFin_iff {n : } {s t : Finset } (hs : ms, m < n) (ht : mt, m < n) :
    s.attachFin hs t.attachFin ht s t
    theorem Finset.attachFin_ssubset_attachFin {n : } {s t : Finset } (hst : s t) (ht : mt, m < n) :
    @[deprecated Finset.attachFin (since := "2025-04-08")]
    def Finset.fin (n : ) (s : Finset ) :

    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
    Instances For
      @[simp, deprecated Finset.mem_attachFin (since := "2025-04-08")]
      theorem Finset.mem_fin {n : } {s : Finset } (a : Fin n) :
      a Finset.fin n s a s
      @[simp, deprecated Finset.coe_attachFin (since := "2025-04-08")]
      theorem Finset.coe_fin (n : ) (s : Finset ) :
      (Finset.fin n s) = Fin.val ⁻¹' s
      @[deprecated Finset.attachFin_subset_attachFin (since := "2025-04-08")]
      @[deprecated Finset.attachFin_subset_attachFin (since := "2025-04-08")]
      theorem Finset.fin_subset_fin (n : ) {s t : Finset } (h : s t) :
      @[simp, deprecated Finset.map_valEmbedding_attachFin (since := "2025-04-08")]
      theorem Finset.fin_map {n : } {s : Finset } :
      map Fin.valEmbedding (Finset.fin n s) = filter (fun (x : ) => x < n) s
      @[deprecated "No replacement" (since := "2025-04-08")]
      theorem Finset.attachFin_eq_fin {n : } {s : Finset } (h : ms, m < n) :