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 : ℕ) : (Finset.range n).val = Multiset.range n

@[simp]

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

@[simp]

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

@[simp]

theorem Finset.range_zero : Finset.range 0 = ∅

@[simp]

theorem Finset.range_one : Finset.range 1 = {0}

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

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

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

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

@[simp]

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

theorem Finset.range_mono : Monotone Finset.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.

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

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

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

@[simp]

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

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

Alias of the reverse direction of Finset.nonempty_range_iff.

@[simp]

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

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

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

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

def notMemRangeEquiv (k : ℕ) : { n : ℕ // n ∉ Multiset.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 ∉ Multiset.range k }) => ↑i - k, invFun := fun (j : ℕ) => ⟨j + k, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

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

@[simp]

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