Finite sets made of a range of elements.

Main declarations

Finset constructions

• Finset.range: For any n : ℕ, range n is equal to {0, 1, ..., n - 1} ⊆ ℕ. This convention is consistent with other languages and normalizes card (range n) = n. Beware, n is not in range n.

Tags

finite sets, finset

range

def Finset.range (n : ℕ) : Finset ℕ

range n is the set of natural numbers less than n.

Equations

• Finset.range n = { val := Multiset.range n, nodup := ⋯ }

@[simp]

theorem Finset.range_val (n : ℕ) : (range n).val = Multiset.range n

@[simp]

theorem Finset.mem_range {n m : ℕ} : m ∈ range n ↔ m < n

@[simp]

theorem Finset.coe_range (n : ℕ) : ↑(range n) = Set.Iio n

@[simp]

theorem Finset.range_zero : range 0 = ∅

@[simp]

theorem Finset.range_one : range 1 = {0}

theorem Finset.range_add_one {n : ℕ} : range (n + 1) = insert n (range n)

@[deprecated Finset.range_add_one (since := "2025-09-08")]

theorem Finset.range_succ {n : ℕ} : range n.succ = insert n (range n)

theorem Finset.notMem_range_self {n : ℕ} : n ∉ range n

@[deprecated Finset.notMem_range_self (since := "2025-05-23")]

theorem Finset.not_mem_range_self {n : ℕ} : n ∉ range n

Alias of Finset.notMem_range_self.

theorem Finset.self_mem_range_succ (n : ℕ) : n ∈ range (n + 1)

theorem Finset.range_subset {n : ℕ} {s : Finset ℕ} : range n ⊆ s ↔ ∀ x < n, x ∈ s

theorem Finset.subset_range {s : Finset ℕ} {n : ℕ} : s ⊆ range n ↔ ∀ x ∈ s, x < n

@[simp]

theorem Finset.range_subset_range {n m : ℕ} : range n ⊆ range m ↔ n ≤ m

theorem Finset.range_mono : Monotone range

theorem GCongr.finset_range_subset_of_le {n m : ℕ} : n ≤ m → Finset.range n ⊆ Finset.range m

Alias of the reverse direction of Finset.range_subset_range.

theorem Finset.mem_range_succ_iff {a b : ℕ} : a ∈ range b.succ ↔ a ≤ b

theorem Finset.mem_range_le {n x : ℕ} (hx : x ∈ range n) : x ≤ n

theorem Finset.mem_range_sub_ne_zero {n x : ℕ} (hx : x ∈ range n) : n - x ≠ 0

@[simp]

theorem Finset.nonempty_range_iff {n : ℕ} : (range n).Nonempty ↔ n ≠ 0

theorem Finset.Aesop.range_nonempty {n : ℕ} : n ≠ 0 → (range n).Nonempty

Alias of the reverse direction of Finset.nonempty_range_iff.

@[simp]

theorem Finset.range_eq_empty_iff {n : ℕ} : range n = ∅ ↔ n = 0

theorem Finset.nonempty_range_add_one {n : ℕ} : (range (n + 1)).Nonempty

@[deprecated Finset.nonempty_range_add_one (since := "2025-09-08")]

theorem Finset.nonempty_range_succ {n : ℕ} : (range (n + 1)).Nonempty

Alias of Finset.nonempty_range_add_one.

theorem Finset.range_nontrivial {n : ℕ} (hn : 1 < n) : (range n).Nontrivial

theorem Finset.exists_nat_subset_range (s : Finset ℕ) : ∃ (n : ℕ), s ⊆ range n

def notMemRangeEquiv (k : ℕ) : { n : ℕ // n ∉ Finset.range k } ≃ ℕ

Equivalence between the set of natural numbers which are ≥ k and ℕ, given by n → n - k.

Equations

• notMemRangeEquiv k = { toFun := fun (i : { n : ℕ // n ∉ Finset.range k }) => ↑i - k, invFun := fun (j : ℕ) => ⟨j + k, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem coe_notMemRangeEquiv (k : ℕ) : ⇑(notMemRangeEquiv k) = fun (i : { n : ℕ // n ∉ Finset.range k }) => ↑i - k

@[simp]

theorem coe_notMemRangeEquiv_symm (k : ℕ) : ⇑(notMemRangeEquiv k).symm = fun (j : ℕ) => ⟨j + k, ⋯⟩