@[reducible]

noncomputable def Set.Finite.toFintype {α : Type u_1} {sa : Set α} (ha : sa.Finite) : Fintype ↑sa

Equations

• ha.toFintype = Finite.toFintype ha

def Set.erase {α : Type u_1} (x : α) (s : Set α) : Set α

Equations

• Set.erase x s = s \ {x}

@[simp]

theorem Set.mem_erase {α : Type u_1} {s : Set α} {z x : α} : z ∈ erase x s ↔ z ≠ x ∧ z ∈ s

theorem Set.erase_eq_of_not_mem {α : Type u_1} {s : Set α} {x : α} (h : x ∉ s) : erase x s = s

theorem Set.insert_erase_eq_of_mem {α : Type u_1} {s : Set α} {x : α} (h : x ∈ s) : insert x (erase x s) = s

@[simp]

theorem Set.finite_erase_iff {α : Type u_1} {s : Set α} {x : α} : (erase x s).Finite ↔ s.Finite

@[simp]

theorem Set.infinite_erase_iff {α : Type u_1} {s : Set α} {x : α} : (erase x s).Infinite ↔ s.Infinite

theorem Set.diff_upair {α : Type u_1} (x y : α) (s : Set α) : s \ {x, y} = (s \ {x}) \ {y}

@[simp]

theorem Set.univ_ne_univ_diff_insert {α : Type u_1} {s : Set α} {x : α} : univ ≠ univ \ insert x s

@[simp]

theorem Set.univ_ne_univ_diff_singleton {α : Type u_1} {x : α} : univ ≠ univ \ {x}

@[simp]

theorem Set.univ_ne_erase {α : Type u_3} {x : α} : univ ≠ erase x univ

theorem Set.diff_erase_self_eq_of_mem {α : Type u_1} {s : Set α} {x : α} (h : x ∈ s) : s \ erase x s = {x}

@[simp]

theorem Set.subsingleton_pair_iff {α : Type u_1} {x y : α} : {x, y}.Subsingleton ↔ x = y

@[simp]

theorem Set.not_nonempty_iff {α : Type u_1} {s : Set α} : ¬s.Nonempty ↔ s = ∅

@[simp]

theorem Set.univ_injOn_iff {α : Type u_1} {β : Type u_2} {f : α → β} : InjOn f univ ↔ Function.Injective f

@[simp]

theorem Set.exists_mem {α : Type u_1} {x : α} : ∃ (s : Set α), x ∈ s

@[simp]

theorem Set.iUnion_preimage {α : Type u_1} {β : Type u_2} {f : α → β} : ⋃ (b : Set β), f ⁻¹' b = univ

theorem Set.minimal_le_minimal_of_subset {α : Type u_1} {s s' : Set α} [ha : LinearOrder α] {x y : α} (h₁ : s' ⊆ s) (h₂ : Minimal (fun (x : α) => x ∈ s') y) (h₃ : Minimal (fun (x : α) => x ∈ s) x) : x ≤ y

theorem Set.eq_empty_iff {α : Type u_1} {s : Set α} : s = ∅ ↔ ∀ (x : α), x ∉ s

theorem Set.ne_empty_iff {α : Type u_1} {s : Set α} : s ≠ ∅ ↔ ∃ (x : α), x ∈ s

theorem Set.ne_empty_of {α : Type u_1} {s : Set α} (x : α) (h : x ∈ s) : s ≠ ∅

@[simp]

theorem Set.erase_singleton {α : Type u_1} {x : α} : erase x {x} = ∅

def Set.filter {α : Type u_1} (s : Set α) (p : α → Prop) : Set α

Equations

• s.filter p = {x : α | x ∈ s ∧ p x}

@[simp]

theorem Set.mem_filter {α : Type u_1} {s : Set α} {p : α → Prop} {x : α} : x ∈ s.filter p ↔ x ∈ s ∧ p x

@[simp]

theorem Set.filter_const_true {α : Type u_1} {s : Set α} : (s.filter fun (x : α) => True) = s

@[simp]

theorem Set.filter_const_false {α : Type u_1} {s : Set α} : (s.filter fun (x : α) => False) = ∅

theorem Set.filter_fn_mem {α : Type u_1} {s s₁ : Set α} : (s.filter fun (x : α) => x ∈ s₁) = s ∩ s₁

theorem Set.forall_not_mem_iff {α : Type u_1} {s : Set α} : (∀ (x : α), x ∉ s) ↔ s = ∅

@[simp]

theorem Set.not_finite_iff_infinite {α : Type u_1} {s : Set α} : ¬s.Finite ↔ s.Infinite

theorem Set.exi_mem_of_infinite {α : Type u_1} {s : Set α} (h : s.Infinite) : ∃ (x : α), x ∈ s

theorem Set.exi_min {α : Type u_1} {s : Set α} [ha : LinearOrder α] (h₁ : s.Finite) (h₂ : s.Nonempty) : ∃ x ∈ s, ∀ y ∈ s, x ≤ y

theorem Set.exi_max {α : Type u_1} {s : Set α} [ha : LinearOrder α] (h₁ : s.Finite) (h₂ : s.Nonempty) : ∃ x ∈ s, ∀ y ∈ s, y ≤ x

@[simp]

theorem Set.filter_empty {α : Type u_1} {p : α → Prop} : ∅.filter p = ∅

theorem Set.finite_iff_exi_finset {α : Type u_1} {s : Set α} : s.Finite ↔ ∃ (s' : Finset α), ↑s' = s

@[simp]

theorem Set.finite_univ_diff_diff_singleton_iff {α : Type u_1} {s : Set α} {x : α} : (univ \ (s \ {x})).Finite ↔ (univ \ s).Finite