Documentation

Mathlib.Data.Finset.Fin

Finsets in Fin n #

A few constructions for Finsets in Fin n.

Main declarations #

source
def Finset.attachFin (s : Finset ℕ) {n : ℕ} (h : ∀ m ∈ s, m < n) :
Finset (Fin 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
      source
      @[simp]
      theorem Finset.mem_attachFin {n : ℕ} {s : Finset ℕ} (h : ∀ m ∈ s, m < n) {a : Fin n} :
      a ∈ s.attachFin h ↔ ↑a ∈ s
      source
      @[simp]
      theorem Finset.coe_attachFin {n : ℕ} {s : Finset ℕ} (h : ∀ m ∈ s, m < n) :
      ↑(s.attachFin h) = Fin.val ⁻¹' ↑s
      source
      @[simp]
      theorem Finset.card_attachFin {n : ℕ} (s : Finset ℕ) (h : ∀ m ∈ s, m < n) :
      (s.attachFin h).card = s.card
      source
      @[simp]
      theorem Finset.image_val_attachFin {n : ℕ} {s : Finset ℕ} (h : ∀ m ∈ s, m < n) :
      image Fin.val (s.attachFin h) = s
      source
      @[simp]
      theorem Finset.map_valEmbedding_attachFin {n : ℕ} {s : Finset ℕ} (h : ∀ m ∈ s, m < n) :
      map Fin.valEmbedding (s.attachFin h) = s
      source
      @[simp]
      theorem Finset.attachFin_subset_attachFin_iff {n : ℕ} {s t : Finset ℕ} (hs : ∀ m ∈ s, m < n) (ht : ∀ m ∈ t, m < n) :
      s.attachFin hs ⊆ t.attachFin ht ↔ s ⊆ t
      source
      theorem Finset.attachFin_subset_attachFin {n : ℕ} {s t : Finset ℕ} (hst : s ⊆ t) (ht : ∀ m ∈ t, m < n) :
      s.attachFin ⋯ ⊆ t.attachFin ht
      source
      @[simp]
      theorem Finset.attachFin_ssubset_attachFin_iff {n : ℕ} {s t : Finset ℕ} (hs : ∀ m ∈ s, m < n) (ht : ∀ m ∈ t, m < n) :
      s.attachFin hs ⊂ t.attachFin ht ↔ s ⊂ t
      source
      theorem Finset.attachFin_ssubset_attachFin {n : ℕ} {s t : Finset ℕ} (hst : s ⊂ t) (ht : ∀ m ∈ t, m < n) :
      s.attachFin ⋯ ⊂ t.attachFin ht
      source
      @[deprecated Finset.attachFin (since := "2025-04-08")]
      def Finset.fin (n : ℕ) (s : Finset ℕ) :
      Finset (Fin n)

      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
          source
          @[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
          source
          @[simp, deprecated Finset.coe_attachFin (since := "2025-04-08")]
          theorem Finset.coe_fin (n : ℕ) (s : Finset ℕ) :
          ↑(Finset.fin n s) = Fin.val ⁻¹' ↑s
          source
          @[deprecated Finset.attachFin_subset_attachFin (since := "2025-04-08")]
          theorem Finset.fin_mono {n : ℕ} :
          Monotone (Finset.fin n)
          source
          @[deprecated Finset.attachFin_subset_attachFin (since := "2025-04-08")]
          theorem Finset.fin_subset_fin (n : ℕ) {s t : Finset ℕ} (h : s ⊆ t) :
          Finset.fin n s ⊆ Finset.fin n t
          source
          @[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
          source
          @[deprecated "No replacement" (since := "2025-04-08")]
          theorem Finset.attachFin_eq_fin {n : ℕ} {s : Finset ℕ} (h : ∀ m ∈ s, m < n) :
          s.attachFin h = Finset.fin n s