mathlib3 documentation

data.finset.fin

Finsets in fin n #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A few constructions for finsets in fin n.

Main declarations #

source
def finset.attach_fin (s : finset ℕ) {n : ℕ} (h : ∀ (m : ℕ), 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.attach_fin h where h is a proof that all elements of s are less than n.

Equations
source
@[simp]
theorem finset.mem_attach_fin {n : ℕ} {s : finset ℕ} (h : ∀ (m : ℕ), m ∈ s → m < n) {a : fin n} :
a ∈ s.attach_fin h ↔ ↑a ∈ s
source
@[simp]
theorem finset.card_attach_fin {n : ℕ} (s : finset ℕ) (h : ∀ (m : ℕ), m ∈ s → m < n) :
(s.attach_fin h).card = s.card