theorem Finset.doubleton_subset {α : Type u_1} {a b : α} {s : Finset α} [DecidableEq α] : {a, b} ⊆ s ↔ a ∈ s ∧ b ∈ s

theorem Finset.no_ssubset_descending_chain {α : Type u_1} {f : ℕ → Finset α} : ¬∀ (i : ℕ), ∃ j > i, f j ⊂ f i

noncomputable def Finset.rangeOfFinite {α : Type u_1} {ι : Sort v} [Finite ι] (f : ι → α) : Finset α

Equations

• Finset.rangeOfFinite f = ⋯.toFinset

theorem Finset.mem_rangeOfFinite_iff {α : Type u_1} {ι : Sort v} [Finite ι] {f : ι → α} {a : α} : a ∈ rangeOfFinite f ↔ ∃ (i : ι), f i = a

noncomputable def Finset.imageOfFinset {α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset α) (f : (a : α) → a ∈ s → β) : Finset β

Equations

• s.imageOfFinset f = s.biUnion fun (x : α) => Finset.rangeOfFinite (f x)

theorem Finset.mem_imageOfFinset_iff {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} {f : (a : α) → a ∈ s → β} {b : β} : b ∈ s.imageOfFinset f ↔ ∃ (a : α) (ha : a ∈ s), f a ha = b

@[simp]

theorem Finset.mem_imageOfFinset {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} (f : (a : α) → a ∈ s → β) (a : α) (ha : a ∈ s) : f a ha ∈ s.imageOfFinset f

theorem Finset.erase_union {α : Type u_1} [DecidableEq α] {a : α} {s t : Finset α} : (s ∪ t).erase a = s.erase a ∪ t.erase a

@[simp]

theorem Finset.equiv_univ {α : Type u_2} {α' : Type u_3} [Fintype α] [Fintype α'] [DecidableEq α'] (e : α ≃ α') : image (⇑e) univ = univ

@[simp]

theorem Finset.sup_univ_equiv {β : Type u_2} {α : Type u_3} {α' : Type u_4} [DecidableEq α] [Fintype α] [Fintype α'] [SemilatticeSup β] [OrderBot β] (f : α → β) (e : α' ≃ α) : (univ.sup fun (i : α') => f (e i)) = univ.sup f

theorem Finset.sup_univ_cast {α : Type u_2} [SemilatticeSup α] [OrderBot α] {n : ℕ} (f : Fin n → α) (n' : ℕ) {h : n' = n} : (univ.sup fun (i : Fin n') => f (Fin.cast h i)) = univ.sup f

theorem Finset.biUnion_eq_empty {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} {f : α → Finset β} : s.biUnion f = ∅ ↔ ∀ i ∈ s, f i = ∅