Basic properties of sets

Sets in Lean are homogeneous; all their elements have the same type. Sets whose elements have type X are thus defined as Set X := X → Prop. Note that this function need not be decidable. The definition is in the module Mathlib.Data.Set.Defs.

This file provides some basic definitions related to sets and functions not present in the definitions file, as well as extra lemmas for functions defined in the definitions file and Mathlib.Data.Set.Operations (empty set, univ, union, intersection, insert, singleton, set-theoretic difference, complement, and powerset).

Note that a set is a term, not a type. There is a coercion from Set α to Type* sending s to the corresponding subtype ↥s.

See also the file SetTheory/ZFC.lean, which contains an encoding of ZFC set theory in Lean.

Main definitions

Notation used here:

• f : α → β is a function,

• s : Set α and s₁ s₂ : Set α are subsets of α

• t : Set β is a subset of β.

Definitions in the file:

• Nonempty s : Prop : the predicate s ≠ ∅. Note that this is the preferred way to express the fact that s has an element (see the Implementation Notes).

• inclusion s₁ s₂ : ↥s₁ → ↥s₂ : the map ↥s₁ → ↥s₂ induced by an inclusion s₁ ⊆ s₂.

Notation

• sᶜ for the complement of s

Implementation notes

• s.Nonempty is to be preferred to s ≠ ∅ or ∃ x, x ∈ s. It has the advantage that the s.Nonempty dot notation can be used.

• For s : Set α, do not use Subtype s. Instead use ↥s or (s : Type*) or s.

Tags

set, sets, subset, subsets, union, intersection, insert, singleton, complement, powerset

Set coercion to a type

instance Set.instBooleanAlgebra {α : Type u} : BooleanAlgebra (Set α)

Equations

• One or more equations did not get rendered due to their size.

instance Set.instHasSSubset {α : Type u} : HasSSubset (Set α)

Equations

• Set.instHasSSubset = { SSubset := fun (x1 x2 : Set α) => x1 < x2 }

@[simp]

theorem Set.top_eq_univ {α : Type u} : ⊤ = univ

@[simp]

theorem Set.bot_eq_empty {α : Type u} : ⊥ = ∅

@[simp]

theorem Set.sup_eq_union {α : Type u} : (fun (x1 x2 : Set α) => x1 ⊔ x2) = fun (x1 x2 : Set α) => x1 ∪ x2

@[simp]

theorem Set.inf_eq_inter {α : Type u} : (fun (x1 x2 : Set α) => x1 ⊓ x2) = fun (x1 x2 : Set α) => x1 ∩ x2

@[simp]

theorem Set.le_eq_subset {α : Type u} : (fun (x1 x2 : Set α) => x1 ≤ x2) = fun (x1 x2 : Set α) => x1 ⊆ x2

@[simp]

theorem Set.lt_eq_ssubset {α : Type u} : (fun (x1 x2 : Set α) => x1 < x2) = fun (x1 x2 : Set α) => x1 ⊂ x2

theorem Set.le_iff_subset {α : Type u} {s t : Set α} : s ≤ t ↔ s ⊆ t

theorem Set.lt_iff_ssubset {α : Type u} {s t : Set α} : s < t ↔ s ⊂ t

theorem LE.le.subset {α : Type u} {s t : Set α} : s ≤ t → s ⊆ t

Alias of the forward direction of Set.le_iff_subset.

theorem HasSubset.Subset.le {α : Type u} {s t : Set α} : s ⊆ t → s ≤ t

Alias of the reverse direction of Set.le_iff_subset.

theorem LT.lt.ssubset {α : Type u} {s t : Set α} : s < t → s ⊂ t

Alias of the forward direction of Set.lt_iff_ssubset.

theorem HasSSubset.SSubset.lt {α : Type u} {s t : Set α} : s ⊂ t → s < t

Alias of the reverse direction of Set.lt_iff_ssubset.

instance Set.PiSetCoe.canLift (ι : Type u) (α : ι → Type v) [∀ (i : ι), Nonempty (α i)] (s : Set ι) : CanLift ((i : ↑s) → α ↑i) ((i : ι) → α i) (fun (f : (i : ι) → α i) (i : ↑s) => f ↑i) fun (x : (i : ↑s) → α ↑i) => True

instance Set.PiSetCoe.canLift' (ι : Type u) (α : Type v) [Nonempty α] (s : Set ι) : CanLift (↑s → α) (ι → α) (fun (f : ι → α) (i : ↑s) => f ↑i) fun (x : ↑s → α) => True

instance instCoeTCElem {α : Type u} (s : Set α) : CoeTC (↑s) α

Equations

• instCoeTCElem s = { coe := fun (x : ↑s) => ↑x }

theorem Set.coe_eq_subtype {α : Type u} (s : Set α) : ↑s = { x : α // x ∈ s }

@[simp]

theorem Set.coe_setOf {α : Type u} (p : α → Prop) : ↑{x : α | p x} = { x : α // p x }

theorem SetCoe.forall {α : Type u} {s : Set α} {p : ↑s → Prop} : (∀ (x : ↑s), p x) ↔ ∀ (x : α) (h : x ∈ s), p ⟨x, h⟩

theorem SetCoe.exists {α : Type u} {s : Set α} {p : ↑s → Prop} : (∃ (x : ↑s), p x) ↔ ∃ (x : α) (h : x ∈ s), p ⟨x, h⟩

theorem SetCoe.exists' {α : Type u} {s : Set α} {p : (x : α) → x ∈ s → Prop} : (∃ (x : α) (h : x ∈ s), p x h) ↔ ∃ (x : ↑s), p ↑x ⋯

theorem SetCoe.forall' {α : Type u} {s : Set α} {p : (x : α) → x ∈ s → Prop} : (∀ (x : α) (h : x ∈ s), p x h) ↔ ∀ (x : ↑s), p ↑x ⋯

@[simp]

theorem set_coe_cast {α : Type u} {s t : Set α} (H' : s = t) (H : ↑s = ↑t) (x : ↑s) : cast H x = ⟨↑x, ⋯⟩

theorem SetCoe.ext {α : Type u} {s : Set α} {a b : ↑s} : ↑a = ↑b → a = b

theorem SetCoe.ext_iff {α : Type u} {s : Set α} {a b : ↑s} : ↑a = ↑b ↔ a = b

theorem Subtype.mem {α : Type u_1} {s : Set α} (p : ↑s) : ↑p ∈ s

See also Subtype.prop

theorem Eq.subset {α : Type u_1} {s t : Set α} : s = t → s ⊆ t

Duplicate of Eq.subset', which currently has elaboration problems.

instance Set.instInhabited {α : Type u} : Inhabited (Set α)

Equations

• Set.instInhabited = { default := ∅ }

theorem Set.mem_of_mem_of_subset {α : Type u} {x : α} {s t : Set α} (hx : x ∈ s) (h : s ⊆ t) : x ∈ t

theorem Set.forall_in_swap {α : Type u} {β : Type v} {s : Set α} {p : α → β → Prop} : (∀ a ∈ s, ∀ (b : β), p a b) ↔ ∀ (b : β), ∀ a ∈ s, p a b

theorem Set.setOf_injective {α : Type u} : Function.Injective setOf

theorem Set.setOf_inj {α : Type u} {p q : α → Prop} : {x : α | p x} = {x : α | q x} ↔ p = q

Lemmas about mem and setOf

theorem Set.mem_setOf {α : Type u} {a : α} {p : α → Prop} : a ∈ {x : α | p x} ↔ p a

theorem Set.eq_mem_setOf {α : Type u} (p : α → Prop) : p = fun (x : α) => x ∈ {a : α | p a}

This lemma is intended for use with rw where a membership predicate is needed, hence the explicit argument and the equality in the reverse direction from normal. See also Set.mem_setOf_eq for the reverse direction applied to an argument.

theorem Membership.mem.out {α : Type u} {p : α → Prop} {a : α} (h : a ∈ {x : α | p x}) : p a

If h : a ∈ {x | p x} then h.out : p x. These are definitionally equal, but this can nevertheless be useful for various reasons, e.g. to apply further projection notation or in an argument to simp.

theorem Set.nmem_setOf_iff {α : Type u} {a : α} {p : α → Prop} : a ∉ {x : α | p x} ↔ ¬p a

@[simp]

theorem Set.setOf_mem_eq {α : Type u} {s : Set α} : {x : α | x ∈ s} = s

theorem Set.setOf_set {α : Type u} {s : Set α} : setOf s = s

theorem Set.setOf_app_iff {α : Type u} {p : α → Prop} {x : α} : {x : α | p x} x ↔ p x

theorem Set.mem_def {α : Type u} {a : α} {s : Set α} : a ∈ s ↔ s a

theorem Set.setOf_bijective {α : Type u} : Function.Bijective setOf

theorem Set.subset_setOf {α : Type u} {p : α → Prop} {s : Set α} : s ⊆ setOf p ↔ ∀ x ∈ s, p x

theorem Set.setOf_subset {α : Type u} {p : α → Prop} {s : Set α} : setOf p ⊆ s ↔ ∀ (x : α), p x → x ∈ s

@[simp]

theorem Set.setOf_subset_setOf {α : Type u} {p q : α → Prop} : {a : α | p a} ⊆ {a : α | q a} ↔ ∀ (a : α), p a → q a

theorem Set.setOf_and {α : Type u} {p q : α → Prop} : {a : α | p a ∧ q a} = {a : α | p a} ∩ {a : α | q a}

theorem Set.setOf_or {α : Type u} {p q : α → Prop} : {a : α | p a ∨ q a} = {a : α | p a} ∪ {a : α | q a}

Subset and strict subset relations

instance Set.instIsReflSubset {α : Type u} : IsRefl (Set α) fun (x1 x2 : Set α) => x1 ⊆ x2

instance Set.instIsTransSubset {α : Type u} : IsTrans (Set α) fun (x1 x2 : Set α) => x1 ⊆ x2

instance Set.instTransSubset {α : Type u} : Trans (fun (x1 x2 : Set α) => x1 ⊆ x2) (fun (x1 x2 : Set α) => x1 ⊆ x2) fun (x1 x2 : Set α) => x1 ⊆ x2

Equations

• Set.instTransSubset = inferInstance

instance Set.instIsAntisymmSubset {α : Type u} : IsAntisymm (Set α) fun (x1 x2 : Set α) => x1 ⊆ x2

instance Set.instIsIrreflSSubset {α : Type u} : IsIrrefl (Set α) fun (x1 x2 : Set α) => x1 ⊂ x2

instance Set.instIsTransSSubset {α : Type u} : IsTrans (Set α) fun (x1 x2 : Set α) => x1 ⊂ x2

instance Set.instTransSSubset {α : Type u} : Trans (fun (x1 x2 : Set α) => x1 ⊂ x2) (fun (x1 x2 : Set α) => x1 ⊂ x2) fun (x1 x2 : Set α) => x1 ⊂ x2

Equations

• Set.instTransSSubset = inferInstance

instance Set.instTransSSubsetSubset {α : Type u} : Trans (fun (x1 x2 : Set α) => x1 ⊂ x2) (fun (x1 x2 : Set α) => x1 ⊆ x2) fun (x1 x2 : Set α) => x1 ⊂ x2

Equations

• Set.instTransSSubsetSubset = inferInstance

instance Set.instTransSubsetSSubset {α : Type u} : Trans (fun (x1 x2 : Set α) => x1 ⊆ x2) (fun (x1 x2 : Set α) => x1 ⊂ x2) fun (x1 x2 : Set α) => x1 ⊂ x2

Equations

• Set.instTransSubsetSSubset = inferInstance

instance Set.instIsAsymmSSubset {α : Type u} : IsAsymm (Set α) fun (x1 x2 : Set α) => x1 ⊂ x2

instance Set.instIsNonstrictStrictOrderSubsetSSubset {α : Type u} : IsNonstrictStrictOrder (Set α) (fun (x1 x2 : Set α) => x1 ⊆ x2) fun (x1 x2 : Set α) => x1 ⊂ x2

theorem Set.subset_def {α : Type u} {s t : Set α} : (s ⊆ t) = ∀ x ∈ s, x ∈ t

theorem Set.ssubset_def {α : Type u} {s t : Set α} : (s ⊂ t) = (s ⊆ t ∧ ¬t ⊆ s)

theorem Set.Subset.refl {α : Type u} (a : Set α) : a ⊆ a

theorem Set.Subset.rfl {α : Type u} {s : Set α} : s ⊆ s

theorem Set.Subset.trans {α : Type u} {a b c : Set α} (ab : a ⊆ b) (bc : b ⊆ c) : a ⊆ c

theorem Set.mem_of_eq_of_mem {α : Type u} {x y : α} {s : Set α} (hx : x = y) (h : y ∈ s) : x ∈ s

theorem Set.Subset.antisymm {α : Type u} {a b : Set α} (h₁ : a ⊆ b) (h₂ : b ⊆ a) : a = b

theorem Set.Subset.antisymm_iff {α : Type u} {a b : Set α} : a = b ↔ a ⊆ b ∧ b ⊆ a

theorem Set.eq_of_subset_of_subset {α : Type u} {a b : Set α} : a ⊆ b → b ⊆ a → a = b

theorem Set.mem_of_subset_of_mem {α : Type u} {s₁ s₂ : Set α} {a : α} (h : s₁ ⊆ s₂) : a ∈ s₁ → a ∈ s₂

theorem Set.not_mem_subset {α : Type u} {a : α} {s t : Set α} (h : s ⊆ t) : a ∉ t → a ∉ s

theorem Set.not_subset {α : Type u} {s t : Set α} : ¬s ⊆ t ↔ ∃ a ∈ s, a ∉ t

theorem Set.not_top_subset {α : Type u} {s : Set α} : ¬⊤ ⊆ s ↔ ∃ (a : α), a ∉ s

theorem Set.eq_of_forall_subset_iff {α : Type u} {s t : Set α} (h : ∀ (u : Set α), s ⊆ u ↔ t ⊆ u) : s = t

Definition of strict subsets s ⊂ t and basic properties.

theorem Set.eq_or_ssubset_of_subset {α : Type u} {s t : Set α} (h : s ⊆ t) : s = t ∨ s ⊂ t

theorem Set.exists_of_ssubset {α : Type u} {s t : Set α} (h : s ⊂ t) : ∃ x ∈ t, x ∉ s

theorem Set.ssubset_iff_subset_ne {α : Type u} {s t : Set α} : s ⊂ t ↔ s ⊆ t ∧ s ≠ t

theorem Set.ssubset_iff_of_subset {α : Type u} {s t : Set α} (h : s ⊆ t) : s ⊂ t ↔ ∃ x ∈ t, x ∉ s

theorem Set.ssubset_iff_exists {α : Type u} {s t : Set α} : s ⊂ t ↔ s ⊆ t ∧ ∃ x ∈ t, x ∉ s

theorem Set.ssubset_of_ssubset_of_subset {α : Type u} {s₁ s₂ s₃ : Set α} (hs₁s₂ : s₁ ⊂ s₂) (hs₂s₃ : s₂ ⊆ s₃) : s₁ ⊂ s₃

theorem Set.ssubset_of_subset_of_ssubset {α : Type u} {s₁ s₂ s₃ : Set α} (hs₁s₂ : s₁ ⊆ s₂) (hs₂s₃ : s₂ ⊂ s₃) : s₁ ⊂ s₃

theorem Set.not_mem_empty {α : Type u} (x : α) : x ∉ ∅

theorem Set.not_not_mem {α : Type u} {a : α} {s : Set α} : ¬a ∉ s ↔ a ∈ s

Non-empty sets

theorem Set.nonempty_coe_sort {α : Type u} {s : Set α} : Nonempty ↑s ↔ s.Nonempty

theorem Set.Nonempty.coe_sort {α : Type u} {s : Set α} : s.Nonempty → Nonempty ↑s

Alias of the reverse direction of Set.nonempty_coe_sort.

theorem Set.nonempty_def {α : Type u} {s : Set α} : s.Nonempty ↔ ∃ (x : α), x ∈ s

theorem Set.nonempty_of_mem {α : Type u} {s : Set α} {x : α} (h : x ∈ s) : s.Nonempty

theorem Set.Nonempty.not_subset_empty {α : Type u} {s : Set α} : s.Nonempty → ¬s ⊆ ∅

noncomputable def Set.Nonempty.some {α : Type u} {s : Set α} (h : s.Nonempty) : α

Extract a witness from s.Nonempty. This function might be used instead of case analysis on the argument. Note that it makes a proof depend on the Classical.choice axiom.

Equations

• h.some = Classical.choose h

theorem Set.Nonempty.some_mem {α : Type u} {s : Set α} (h : s.Nonempty) : h.some ∈ s

theorem Set.Nonempty.mono {α : Type u} {s t : Set α} (ht : s ⊆ t) (hs : s.Nonempty) : t.Nonempty

theorem Set.nonempty_of_not_subset {α : Type u} {s t : Set α} (h : ¬s ⊆ t) : (s \ t).Nonempty

theorem Set.nonempty_of_ssubset {α : Type u} {s t : Set α} (ht : s ⊂ t) : (t \ s).Nonempty

theorem Set.Nonempty.of_diff {α : Type u} {s t : Set α} (h : (s \ t).Nonempty) : s.Nonempty

theorem Set.nonempty_of_ssubset' {α : Type u} {s t : Set α} (ht : s ⊂ t) : t.Nonempty

theorem Set.Nonempty.inl {α : Type u} {s t : Set α} (hs : s.Nonempty) : (s ∪ t).Nonempty

theorem Set.Nonempty.inr {α : Type u} {s t : Set α} (ht : t.Nonempty) : (s ∪ t).Nonempty

@[simp]

theorem Set.union_nonempty {α : Type u} {s t : Set α} : (s ∪ t).Nonempty ↔ s.Nonempty ∨ t.Nonempty

theorem Set.Nonempty.left {α : Type u} {s t : Set α} (h : (s ∩ t).Nonempty) : s.Nonempty

theorem Set.Nonempty.right {α : Type u} {s t : Set α} (h : (s ∩ t).Nonempty) : t.Nonempty

theorem Set.inter_nonempty {α : Type u} {s t : Set α} : (s ∩ t).Nonempty ↔ ∃ x ∈ s, x ∈ t

theorem Set.inter_nonempty_iff_exists_left {α : Type u} {s t : Set α} : (s ∩ t).Nonempty ↔ ∃ x ∈ s, x ∈ t

theorem Set.inter_nonempty_iff_exists_right {α : Type u} {s t : Set α} : (s ∩ t).Nonempty ↔ ∃ x ∈ t, x ∈ s

theorem Set.nonempty_iff_univ_nonempty {α : Type u} : Nonempty α ↔ univ.Nonempty

@[simp]

theorem Set.univ_nonempty {α : Type u} [Nonempty α] : univ.Nonempty

theorem Set.Nonempty.to_subtype {α : Type u} {s : Set α} : s.Nonempty → Nonempty ↑s

theorem Set.Nonempty.to_type {α : Type u} {s : Set α} : s.Nonempty → Nonempty α

instance Set.univ.nonempty {α : Type u} [Nonempty α] : Nonempty ↑univ

instance Set.instNonemptyTop {α : Type u} [Nonempty α] : Nonempty ↑⊤

theorem Set.Nonempty.of_subtype {α : Type u} {s : Set α} [Nonempty ↑s] : s.Nonempty

@[deprecated Set.Nonempty.of_subtype (since := "2024-11-23")]

theorem Set.nonempty_of_nonempty_subtype {α : Type u} {s : Set α} [Nonempty ↑s] : s.Nonempty

Alias of Set.Nonempty.of_subtype.

Lemmas about the empty set

theorem Set.empty_def {α : Type u} : ∅ = {_x : α | False}

@[simp]

theorem Set.mem_empty_iff_false {α : Type u} (x : α) : x ∈ ∅ ↔ False

@[simp]

theorem Set.setOf_false {α : Type u} : {_a : α | False} = ∅

@[simp]

theorem Set.setOf_bot {α : Type u} : {_x : α | ⊥} = ∅

@[simp]

theorem Set.empty_subset {α : Type u} (s : Set α) : ∅ ⊆ s

@[simp]

theorem Set.subset_empty_iff {α : Type u} {s : Set α} : s ⊆ ∅ ↔ s = ∅

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

theorem Set.eq_empty_of_forall_not_mem {α : Type u} {s : Set α} (h : ∀ (x : α), x ∉ s) : s = ∅

theorem Set.eq_empty_of_subset_empty {α : Type u} {s : Set α} : s ⊆ ∅ → s = ∅

theorem Set.eq_empty_of_isEmpty {α : Type u} [IsEmpty α] (s : Set α) : s = ∅

instance Set.uniqueEmpty {α : Type u} [IsEmpty α] : Unique (Set α)

There is exactly one set of a type that is empty.

Equations

• Set.uniqueEmpty = { default := ∅, uniq := ⋯ }

theorem Set.not_nonempty_iff_eq_empty {α : Type u} {s : Set α} : ¬s.Nonempty ↔ s = ∅

See also Set.nonempty_iff_ne_empty.

theorem Set.nonempty_iff_ne_empty {α : Type u} {s : Set α} : s.Nonempty ↔ s ≠ ∅

See also Set.not_nonempty_iff_eq_empty.

theorem Set.not_nonempty_iff_eq_empty' {α : Type u} {s : Set α} : ¬Nonempty ↑s ↔ s = ∅

See also nonempty_iff_ne_empty'.

theorem Set.nonempty_iff_ne_empty' {α : Type u} {s : Set α} : Nonempty ↑s ↔ s ≠ ∅

See also not_nonempty_iff_eq_empty'.

theorem Set.Nonempty.ne_empty {α : Type u} {s : Set α} : s.Nonempty → s ≠ ∅

Alias of the forward direction of Set.nonempty_iff_ne_empty.

---

See also Set.not_nonempty_iff_eq_empty.

@[simp]

theorem Set.not_nonempty_empty {α : Type u} : ¬∅.Nonempty

@[simp]

theorem Set.isEmpty_coe_sort {α : Type u} {s : Set α} : IsEmpty ↑s ↔ s = ∅

theorem Set.eq_empty_or_nonempty {α : Type u} (s : Set α) : s = ∅ ∨ s.Nonempty

theorem Set.subset_eq_empty {α : Type u} {s t : Set α} (h : t ⊆ s) (e : s = ∅) : t = ∅

theorem Set.forall_mem_empty {α : Type u} {p : α → Prop} : (∀ x ∈ ∅, p x) ↔ True

instance Set.instIsEmptyElemEmptyCollection (α : Type u) : IsEmpty ↑∅

@[simp]

theorem Set.empty_ssubset {α : Type u} {s : Set α} : ∅ ⊂ s ↔ s.Nonempty

theorem Set.Nonempty.empty_ssubset {α : Type u} {s : Set α} : s.Nonempty → ∅ ⊂ s

Alias of the reverse direction of Set.empty_ssubset.

Universal set.

In Lean @univ α (or univ : Set α) is the set that contains all elements of type α. Mathematically it is the same as α but it has a different type.

@[simp]

theorem Set.setOf_true {α : Type u} : {_x : α | True} = univ

@[simp]

theorem Set.setOf_top {α : Type u} : {_x : α | ⊤} = univ

@[simp]

theorem Set.univ_eq_empty_iff {α : Type u} : univ = ∅ ↔ IsEmpty α

theorem Set.empty_ne_univ {α : Type u} [Nonempty α] : ∅ ≠ univ

@[simp]

theorem Set.subset_univ {α : Type u} (s : Set α) : s ⊆ univ

@[simp]

theorem Set.univ_subset_iff {α : Type u} {s : Set α} : univ ⊆ s ↔ s = univ

theorem Set.eq_univ_of_univ_subset {α : Type u} {s : Set α} : univ ⊆ s → s = univ

Alias of the forward direction of Set.univ_subset_iff.

theorem Set.eq_univ_iff_forall {α : Type u} {s : Set α} : s = univ ↔ ∀ (x : α), x ∈ s

theorem Set.eq_univ_of_forall {α : Type u} {s : Set α} : (∀ (x : α), x ∈ s) → s = univ

theorem Set.Nonempty.eq_univ {α : Type u} {s : Set α} [Subsingleton α] : s.Nonempty → s = univ

theorem Set.eq_univ_of_subset {α : Type u} {s t : Set α} (h : s ⊆ t) (hs : s = univ) : t = univ

theorem Set.exists_mem_of_nonempty (α : Type u_1) [Nonempty α] : ∃ (x : α), x ∈ univ

theorem Set.ne_univ_iff_exists_not_mem {α : Type u_1} (s : Set α) : s ≠ univ ↔ ∃ (a : α), a ∉ s

theorem Set.not_subset_iff_exists_mem_not_mem {α : Type u_1} {s t : Set α} : ¬s ⊆ t ↔ ∃ x ∈ s, x ∉ t

theorem Set.univ_unique {α : Type u} [Unique α] : univ = {default}

theorem Set.ssubset_univ_iff {α : Type u} {s : Set α} : s ⊂ univ ↔ s ≠ univ

instance Set.nontrivial_of_nonempty {α : Type u} [Nonempty α] : Nontrivial (Set α)

Lemmas about union

theorem Set.union_def {α : Type u} {s₁ s₂ : Set α} : s₁ ∪ s₂ = {a : α | a ∈ s₁ ∨ a ∈ s₂}

theorem Set.mem_union_left {α : Type u} {x : α} {a : Set α} (b : Set α) : x ∈ a → x ∈ a ∪ b

theorem Set.mem_union_right {α : Type u} {x : α} {b : Set α} (a : Set α) : x ∈ b → x ∈ a ∪ b

theorem Set.mem_or_mem_of_mem_union {α : Type u} {x : α} {a b : Set α} (H : x ∈ a ∪ b) : x ∈ a ∨ x ∈ b

theorem Set.MemUnion.elim {α : Type u} {x : α} {a b : Set α} {P : Prop} (H₁ : x ∈ a ∪ b) (H₂ : x ∈ a → P) (H₃ : x ∈ b → P) : P

@[simp]

theorem Set.mem_union {α : Type u} (x : α) (a b : Set α) : x ∈ a ∪ b ↔ x ∈ a ∨ x ∈ b

@[simp]

theorem Set.union_self {α : Type u} (a : Set α) : a ∪ a = a

@[simp]

theorem Set.union_empty {α : Type u} (a : Set α) : a ∪ ∅ = a

@[simp]

theorem Set.empty_union {α : Type u} (a : Set α) : ∅ ∪ a = a

theorem Set.union_comm {α : Type u} (a b : Set α) : a ∪ b = b ∪ a

theorem Set.union_assoc {α : Type u} (a b c : Set α) : a ∪ b ∪ c = a ∪ (b ∪ c)

instance Set.union_isAssoc {α : Type u} : Std.Associative fun (x1 x2 : Set α) => x1 ∪ x2

instance Set.union_isComm {α : Type u} : Std.Commutative fun (x1 x2 : Set α) => x1 ∪ x2

theorem Set.union_left_comm {α : Type u} (s₁ s₂ s₃ : Set α) : s₁ ∪ (s₂ ∪ s₃) = s₂ ∪ (s₁ ∪ s₃)

theorem Set.union_right_comm {α : Type u} (s₁ s₂ s₃ : Set α) : s₁ ∪ s₂ ∪ s₃ = s₁ ∪ s₃ ∪ s₂

@[simp]

theorem Set.union_eq_left {α : Type u} {s t : Set α} : s ∪ t = s ↔ t ⊆ s

@[simp]

theorem Set.union_eq_right {α : Type u} {s t : Set α} : s ∪ t = t ↔ s ⊆ t

theorem Set.union_eq_self_of_subset_left {α : Type u} {s t : Set α} (h : s ⊆ t) : s ∪ t = t

theorem Set.union_eq_self_of_subset_right {α : Type u} {s t : Set α} (h : t ⊆ s) : s ∪ t = s

@[simp]

theorem Set.subset_union_left {α : Type u} {s t : Set α} : s ⊆ s ∪ t

@[simp]

theorem Set.subset_union_right {α : Type u} {s t : Set α} : t ⊆ s ∪ t

theorem Set.union_subset {α : Type u} {s t r : Set α} (sr : s ⊆ r) (tr : t ⊆ r) : s ∪ t ⊆ r

@[simp]

theorem Set.union_subset_iff {α : Type u} {s t u : Set α} : s ∪ t ⊆ u ↔ s ⊆ u ∧ t ⊆ u

theorem Set.union_subset_union {α : Type u} {s₁ s₂ t₁ t₂ : Set α} (h₁ : s₁ ⊆ s₂) (h₂ : t₁ ⊆ t₂) : s₁ ∪ t₁ ⊆ s₂ ∪ t₂

theorem Set.union_subset_union_left {α : Type u} {s₁ s₂ : Set α} (t : Set α) (h : s₁ ⊆ s₂) : s₁ ∪ t ⊆ s₂ ∪ t

theorem Set.union_subset_union_right {α : Type u} (s : Set α) {t₁ t₂ : Set α} (h : t₁ ⊆ t₂) : s ∪ t₁ ⊆ s ∪ t₂

theorem Set.subset_union_of_subset_left {α : Type u} {s t : Set α} (h : s ⊆ t) (u : Set α) : s ⊆ t ∪ u

theorem Set.subset_union_of_subset_right {α : Type u} {s u : Set α} (h : s ⊆ u) (t : Set α) : s ⊆ t ∪ u

theorem Set.union_congr_left {α : Type u} {s t u : Set α} (ht : t ⊆ s ∪ u) (hu : u ⊆ s ∪ t) : s ∪ t = s ∪ u

theorem Set.union_congr_right {α : Type u} {s t u : Set α} (hs : s ⊆ t ∪ u) (ht : t ⊆ s ∪ u) : s ∪ u = t ∪ u

theorem Set.union_eq_union_iff_left {α : Type u} {s t u : Set α} : s ∪ t = s ∪ u ↔ t ⊆ s ∪ u ∧ u ⊆ s ∪ t

theorem Set.union_eq_union_iff_right {α : Type u} {s t u : Set α} : s ∪ u = t ∪ u ↔ s ⊆ t ∪ u ∧ t ⊆ s ∪ u

@[simp]

theorem Set.union_empty_iff {α : Type u} {s t : Set α} : s ∪ t = ∅ ↔ s = ∅ ∧ t = ∅

@[simp]

theorem Set.union_univ {α : Type u} (s : Set α) : s ∪ univ = univ

@[simp]

theorem Set.univ_union {α : Type u} (s : Set α) : univ ∪ s = univ

@[simp]

theorem Set.ssubset_union_left_iff {α : Type u} {s t : Set α} : s ⊂ s ∪ t ↔ ¬t ⊆ s

@[simp]

theorem Set.ssubset_union_right_iff {α : Type u} {s t : Set α} : t ⊂ s ∪ t ↔ ¬s ⊆ t

Lemmas about intersection

theorem Set.inter_def {α : Type u} {s₁ s₂ : Set α} : s₁ ∩ s₂ = {a : α | a ∈ s₁ ∧ a ∈ s₂}

@[simp]

theorem Set.mem_inter_iff {α : Type u} (x : α) (a b : Set α) : x ∈ a ∩ b ↔ x ∈ a ∧ x ∈ b

theorem Set.mem_inter {α : Type u} {x : α} {a b : Set α} (ha : x ∈ a) (hb : x ∈ b) : x ∈ a ∩ b

theorem Set.mem_of_mem_inter_left {α : Type u} {x : α} {a b : Set α} (h : x ∈ a ∩ b) : x ∈ a

theorem Set.mem_of_mem_inter_right {α : Type u} {x : α} {a b : Set α} (h : x ∈ a ∩ b) : x ∈ b

@[simp]

theorem Set.inter_self {α : Type u} (a : Set α) : a ∩ a = a

@[simp]

theorem Set.inter_empty {α : Type u} (a : Set α) : a ∩ ∅ = ∅

@[simp]

theorem Set.empty_inter {α : Type u} (a : Set α) : ∅ ∩ a = ∅

theorem Set.inter_comm {α : Type u} (a b : Set α) : a ∩ b = b ∩ a

theorem Set.inter_assoc {α : Type u} (a b c : Set α) : a ∩ b ∩ c = a ∩ (b ∩ c)

instance Set.inter_isAssoc {α : Type u} : Std.Associative fun (x1 x2 : Set α) => x1 ∩ x2

instance Set.inter_isComm {α : Type u} : Std.Commutative fun (x1 x2 : Set α) => x1 ∩ x2

theorem Set.inter_left_comm {α : Type u} (s₁ s₂ s₃ : Set α) : s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃)

theorem Set.inter_right_comm {α : Type u} (s₁ s₂ s₃ : Set α) : s₁ ∩ s₂ ∩ s₃ = s₁ ∩ s₃ ∩ s₂

@[simp]

theorem Set.inter_subset_left {α : Type u} {s t : Set α} : s ∩ t ⊆ s

@[simp]

theorem Set.inter_subset_right {α : Type u} {s t : Set α} : s ∩ t ⊆ t

theorem Set.subset_inter {α : Type u} {s t r : Set α} (rs : r ⊆ s) (rt : r ⊆ t) : r ⊆ s ∩ t

@[simp]

theorem Set.subset_inter_iff {α : Type u} {s t r : Set α} : r ⊆ s ∩ t ↔ r ⊆ s ∧ r ⊆ t

@[simp]

theorem Set.inter_eq_left {α : Type u} {s t : Set α} : s ∩ t = s ↔ s ⊆ t

@[simp]

theorem Set.inter_eq_right {α : Type u} {s t : Set α} : s ∩ t = t ↔ t ⊆ s

@[simp]

theorem Set.left_eq_inter {α : Type u} {s t : Set α} : s = s ∩ t ↔ s ⊆ t

@[simp]

theorem Set.right_eq_inter {α : Type u} {s t : Set α} : t = s ∩ t ↔ t ⊆ s

theorem Set.inter_eq_self_of_subset_left {α : Type u} {s t : Set α} : s ⊆ t → s ∩ t = s

theorem Set.inter_eq_self_of_subset_right {α : Type u} {s t : Set α} : t ⊆ s → s ∩ t = t

theorem Set.inter_congr_left {α : Type u} {s t u : Set α} (ht : s ∩ u ⊆ t) (hu : s ∩ t ⊆ u) : s ∩ t = s ∩ u

theorem Set.inter_congr_right {α : Type u} {s t u : Set α} (hs : t ∩ u ⊆ s) (ht : s ∩ u ⊆ t) : s ∩ u = t ∩ u

theorem Set.inter_eq_inter_iff_left {α : Type u} {s t u : Set α} : s ∩ t = s ∩ u ↔ s ∩ u ⊆ t ∧ s ∩ t ⊆ u

theorem Set.inter_eq_inter_iff_right {α : Type u} {s t u : Set α} : s ∩ u = t ∩ u ↔ t ∩ u ⊆ s ∧ s ∩ u ⊆ t

@[simp]

theorem Set.inter_univ {α : Type u} (a : Set α) : a ∩ univ = a

@[simp]

theorem Set.univ_inter {α : Type u} (a : Set α) : univ ∩ a = a

theorem Set.inter_subset_inter {α : Type u} {s₁ s₂ t₁ t₂ : Set α} (h₁ : s₁ ⊆ t₁) (h₂ : s₂ ⊆ t₂) : s₁ ∩ s₂ ⊆ t₁ ∩ t₂

theorem Set.inter_subset_inter_left {α : Type u} {s t : Set α} (u : Set α) (H : s ⊆ t) : s ∩ u ⊆ t ∩ u

theorem Set.inter_subset_inter_right {α : Type u} {s t : Set α} (u : Set α) (H : s ⊆ t) : u ∩ s ⊆ u ∩ t

theorem Set.union_inter_cancel_left {α : Type u} {s t : Set α} : (s ∪ t) ∩ s = s

theorem Set.union_inter_cancel_right {α : Type u} {s t : Set α} : (s ∪ t) ∩ t = t

theorem Set.inter_setOf_eq_sep {α : Type u} (s : Set α) (p : α → Prop) : s ∩ {a : α | p a} = {a : α | a ∈ s ∧ p a}

theorem Set.setOf_inter_eq_sep {α : Type u} (p : α → Prop) (s : Set α) : {a : α | p a} ∩ s = {a : α | a ∈ s ∧ p a}

@[simp]

theorem Set.inter_ssubset_right_iff {α : Type u} {s t : Set α} : s ∩ t ⊂ t ↔ ¬t ⊆ s

@[simp]

theorem Set.inter_ssubset_left_iff {α : Type u} {s t : Set α} : s ∩ t ⊂ s ↔ ¬s ⊆ t

Distributivity laws

theorem Set.inter_union_distrib_left {α : Type u} (s t u : Set α) : s ∩ (t ∪ u) = s ∩ t ∪ s ∩ u

theorem Set.union_inter_distrib_right {α : Type u} (s t u : Set α) : (s ∪ t) ∩ u = s ∩ u ∪ t ∩ u

theorem Set.union_inter_distrib_left {α : Type u} (s t u : Set α) : s ∪ t ∩ u = (s ∪ t) ∩ (s ∪ u)

theorem Set.inter_union_distrib_right {α : Type u} (s t u : Set α) : s ∩ t ∪ u = (s ∪ u) ∩ (t ∪ u)

theorem Set.union_union_distrib_left {α : Type u} (s t u : Set α) : s ∪ (t ∪ u) = s ∪ t ∪ (s ∪ u)

theorem Set.union_union_distrib_right {α : Type u} (s t u : Set α) : s ∪ t ∪ u = s ∪ u ∪ (t ∪ u)

theorem Set.inter_inter_distrib_left {α : Type u} (s t u : Set α) : s ∩ (t ∩ u) = s ∩ t ∩ (s ∩ u)

theorem Set.inter_inter_distrib_right {α : Type u} (s t u : Set α) : s ∩ t ∩ u = s ∩ u ∩ (t ∩ u)

theorem Set.union_union_union_comm {α : Type u} (s t u v : Set α) : s ∪ t ∪ (u ∪ v) = s ∪ u ∪ (t ∪ v)

theorem Set.inter_inter_inter_comm {α : Type u} (s t u v : Set α) : s ∩ t ∩ (u ∩ v) = s ∩ u ∩ (t ∩ v)

Lemmas about sets defined as {x ∈ s | p x}.

theorem Set.mem_sep {α : Type u} {s : Set α} {p : α → Prop} {x : α} (xs : x ∈ s) (px : p x) : x ∈ {x : α | x ∈ s ∧ p x}

@[simp]

theorem Set.sep_mem_eq {α : Type u} {s t : Set α} : {x : α | x ∈ s ∧ x ∈ t} = s ∩ t

@[simp]

theorem Set.mem_sep_iff {α : Type u} {s : Set α} {p : α → Prop} {x : α} : x ∈ {x : α | x ∈ s ∧ p x} ↔ x ∈ s ∧ p x

theorem Set.sep_ext_iff {α : Type u} {s : Set α} {p q : α → Prop} : {x : α | x ∈ s ∧ p x} = {x : α | x ∈ s ∧ q x} ↔ ∀ x ∈ s, p x ↔ q x

theorem Set.sep_eq_of_subset {α : Type u} {s t : Set α} (h : s ⊆ t) : {x : α | x ∈ t ∧ x ∈ s} = s

@[simp]

theorem Set.sep_subset {α : Type u} (s : Set α) (p : α → Prop) : {x : α | x ∈ s ∧ p x} ⊆ s

@[simp]

theorem Set.sep_eq_self_iff_mem_true {α : Type u} {s : Set α} {p : α → Prop} : {x : α | x ∈ s ∧ p x} = s ↔ ∀ x ∈ s, p x

@[simp]

theorem Set.sep_eq_empty_iff_mem_false {α : Type u} {s : Set α} {p : α → Prop} : {x : α | x ∈ s ∧ p x} = ∅ ↔ ∀ x ∈ s, ¬p x

theorem Set.sep_true {α : Type u} {s : Set α} : {x : α | x ∈ s ∧ True} = s

theorem Set.sep_false {α : Type u} {s : Set α} : {x : α | x ∈ s ∧ False} = ∅

theorem Set.sep_empty {α : Type u} (p : α → Prop) : {x : α | x ∈ ∅ ∧ p x} = ∅

theorem Set.sep_univ {α : Type u} {p : α → Prop} : {x : α | x ∈ univ ∧ p x} = {x : α | p x}

@[simp]

theorem Set.sep_union {α : Type u} {s t : Set α} {p : α → Prop} : {x : α | (x ∈ s ∨ x ∈ t) ∧ p x} = {x : α | x ∈ s ∧ p x} ∪ {x : α | x ∈ t ∧ p x}

@[simp]

theorem Set.sep_inter {α : Type u} {s t : Set α} {p : α → Prop} : {x : α | (x ∈ s ∧ x ∈ t) ∧ p x} = {x : α | x ∈ s ∧ p x} ∩ {x : α | x ∈ t ∧ p x}

@[simp]

theorem Set.sep_and {α : Type u} {s : Set α} {p q : α → Prop} : {x : α | x ∈ s ∧ p x ∧ q x} = {x : α | x ∈ s ∧ p x} ∩ {x : α | x ∈ s ∧ q x}

@[simp]

theorem Set.sep_or {α : Type u} {s : Set α} {p q : α → Prop} : {x : α | x ∈ s ∧ (p x ∨ q x)} = {x : α | x ∈ s ∧ p x} ∪ {x : α | x ∈ s ∧ q x}

@[simp]

theorem Set.sep_setOf {α : Type u} {p q : α → Prop} : {x : α | x ∈ {y : α | p y} ∧ q x} = {x : α | p x ∧ q x}

theorem Set.inter_diff_assoc {α : Type u} (a b c : Set α) : (a ∩ b) \ c = a ∩ (b \ c)

See also Set.sdiff_inter_right_comm.

theorem Set.sdiff_inter_right_comm {α : Type u} (s t u : Set α) : s \ t ∩ u = (s ∩ u) \ t

See also Set.inter_diff_assoc.

theorem Set.inter_sdiff_left_comm {α : Type u} (s t u : Set α) : s ∩ (t \ u) = t ∩ (s \ u)

theorem Set.diff_union_diff_cancel {α : Type u} {s t u : Set α} (hts : t ⊆ s) (hut : u ⊆ t) : s \ t ∪ t \ u = s \ u

theorem Set.diff_union_diff_cancel' {α : Type u} {s t u : Set α} (hi : s ∩ u ⊆ t) (hu : t ⊆ s ∪ u) : s \ t ∪ t \ u = s \ u

A version of diff_union_diff_cancel with more general hypotheses.

theorem Set.diff_diff_eq_sdiff_union {α : Type u} {s t u : Set α} (h : u ⊆ s) : s \ (t \ u) = s \ t ∪ u

theorem Set.inter_diff_distrib_left {α : Type u} (s t u : Set α) : s ∩ (t \ u) = (s ∩ t) \ (s ∩ u)

theorem Set.inter_diff_distrib_right {α : Type u} (s t u : Set α) : s \ t ∩ u = (s ∩ u) \ (t ∩ u)

theorem Set.diff_inter_distrib_right {α : Type u} (s t r : Set α) : (t ∩ r) \ s = t \ s ∩ (r \ s)

Lemmas about complement

theorem Set.compl_def {α : Type u} (s : Set α) : sᶜ = {x : α | x ∉ s}

theorem Set.mem_compl {α : Type u} {s : Set α} {x : α} (h : x ∉ s) : x ∈ sᶜ

theorem Set.compl_setOf {α : Type u_1} (p : α → Prop) : {a : α | p a}ᶜ = {a : α | ¬p a}

theorem Set.not_mem_of_mem_compl {α : Type u} {s : Set α} {x : α} (h : x ∈ sᶜ) : x ∉ s

theorem Set.not_mem_compl_iff {α : Type u} {s : Set α} {x : α} : x ∉ sᶜ ↔ x ∈ s

@[simp]

theorem Set.inter_compl_self {α : Type u} (s : Set α) : s ∩ sᶜ = ∅

@[simp]

theorem Set.compl_inter_self {α : Type u} (s : Set α) : sᶜ ∩ s = ∅

@[simp]

theorem Set.compl_empty {α : Type u} : ∅ᶜ = univ

@[simp]

theorem Set.compl_union {α : Type u} (s t : Set α) : (s ∪ t)ᶜ = sᶜ ∩ tᶜ

theorem Set.compl_inter {α : Type u} (s t : Set α) : (s ∩ t)ᶜ = sᶜ ∪ tᶜ

@[simp]

theorem Set.compl_univ {α : Type u} : univᶜ = ∅

@[simp]

theorem Set.compl_empty_iff {α : Type u} {s : Set α} : sᶜ = ∅ ↔ s = univ

@[simp]

theorem Set.compl_univ_iff {α : Type u} {s : Set α} : sᶜ = univ ↔ s = ∅

theorem Set.compl_ne_univ {α : Type u} {s : Set α} : sᶜ ≠ univ ↔ s.Nonempty

theorem Set.inl_compl_union_inr_compl {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} : Sum.inl '' sᶜ ∪ Sum.inr '' tᶜ = (Sum.inl '' s ∪ Sum.inr '' t)ᶜ

theorem Set.nonempty_compl {α : Type u} {s : Set α} : sᶜ.Nonempty ↔ s ≠ univ

theorem Set.union_eq_compl_compl_inter_compl {α : Type u} (s t : Set α) : s ∪ t = (sᶜ ∩ tᶜ)ᶜ

theorem Set.inter_eq_compl_compl_union_compl {α : Type u} (s t : Set α) : s ∩ t = (sᶜ ∪ tᶜ)ᶜ

@[simp]

theorem Set.union_compl_self {α : Type u} (s : Set α) : s ∪ sᶜ = univ

@[simp]

theorem Set.compl_union_self {α : Type u} (s : Set α) : sᶜ ∪ s = univ

theorem Set.compl_subset_comm {α : Type u} {s t : Set α} : sᶜ ⊆ t ↔ tᶜ ⊆ s

theorem Set.subset_compl_comm {α : Type u} {s t : Set α} : s ⊆ tᶜ ↔ t ⊆ sᶜ

@[simp]

theorem Set.compl_subset_compl {α : Type u} {s t : Set α} : sᶜ ⊆ tᶜ ↔ t ⊆ s

theorem Set.compl_subset_compl_of_subset {α : Type u} {s t : Set α} (h : t ⊆ s) : sᶜ ⊆ tᶜ

theorem Set.subset_union_compl_iff_inter_subset {α : Type u} {s t u : Set α} : s ⊆ t ∪ uᶜ ↔ s ∩ u ⊆ t

theorem Set.compl_subset_iff_union {α : Type u} {s t : Set α} : sᶜ ⊆ t ↔ s ∪ t = univ

theorem Set.inter_subset {α : Type u} (a b c : Set α) : a ∩ b ⊆ c ↔ a ⊆ bᶜ ∪ c

theorem Set.inter_compl_nonempty_iff {α : Type u} {s t : Set α} : (s ∩ tᶜ).Nonempty ↔ ¬s ⊆ t

Lemmas about set difference

theorem Set.not_mem_diff_of_mem {α : Type u} {s t : Set α} {x : α} (hx : x ∈ t) : x ∉ s \ t

theorem Set.mem_of_mem_diff {α : Type u} {s t : Set α} {x : α} (h : x ∈ s \ t) : x ∈ s

theorem Set.not_mem_of_mem_diff {α : Type u} {s t : Set α} {x : α} (h : x ∈ s \ t) : x ∉ t

theorem Set.diff_eq_compl_inter {α : Type u} {s t : Set α} : s \ t = tᶜ ∩ s

theorem Set.diff_nonempty {α : Type u} {s t : Set α} : (s \ t).Nonempty ↔ ¬s ⊆ t

theorem Set.diff_subset {α : Type u} {s t : Set α} : s \ t ⊆ s

theorem Set.diff_subset_compl {α : Type u} (s t : Set α) : s \ t ⊆ tᶜ

theorem Set.union_diff_cancel' {α : Type u} {s t u : Set α} (h₁ : s ⊆ t) (h₂ : t ⊆ u) : t ∪ u \ s = u

theorem Set.union_diff_cancel {α : Type u} {s t : Set α} (h : s ⊆ t) : s ∪ t \ s = t

theorem Set.union_diff_cancel_left {α : Type u} {s t : Set α} (h : s ∩ t ⊆ ∅) : (s ∪ t) \ s = t

theorem Set.union_diff_cancel_right {α : Type u} {s t : Set α} (h : s ∩ t ⊆ ∅) : (s ∪ t) \ t = s

@[simp]

theorem Set.union_diff_left {α : Type u} {s t : Set α} : (s ∪ t) \ s = t \ s

@[simp]

theorem Set.union_diff_right {α : Type u} {s t : Set α} : (s ∪ t) \ t = s \ t

theorem Set.union_diff_distrib {α : Type u} {s t u : Set α} : (s ∪ t) \ u = s \ u ∪ t \ u

@[simp]

theorem Set.inter_diff_self {α : Type u} (a b : Set α) : a ∩ (b \ a) = ∅

@[simp]

theorem Set.inter_union_diff {α : Type u} (s t : Set α) : s ∩ t ∪ s \ t = s

@[simp]

theorem Set.diff_union_inter {α : Type u} (s t : Set α) : s \ t ∪ s ∩ t = s

@[simp]

theorem Set.inter_union_compl {α : Type u} (s t : Set α) : s ∩ t ∪ s ∩ tᶜ = s

theorem Set.diff_subset_diff {α : Type u} {s₁ s₂ t₁ t₂ : Set α} : s₁ ⊆ s₂ → t₂ ⊆ t₁ → s₁ \ t₁ ⊆ s₂ \ t₂

theorem Set.diff_subset_diff_left {α : Type u} {s₁ s₂ t : Set α} (h : s₁ ⊆ s₂) : s₁ \ t ⊆ s₂ \ t

theorem Set.diff_subset_diff_right {α : Type u} {s t u : Set α} (h : t ⊆ u) : s \ u ⊆ s \ t

theorem Set.diff_subset_diff_iff_subset {α : Type u} {s t r : Set α} (hs : s ⊆ r) (ht : t ⊆ r) : r \ s ⊆ r \ t ↔ t ⊆ s

theorem Set.compl_eq_univ_diff {α : Type u} (s : Set α) : sᶜ = univ \ s

@[simp]

theorem Set.empty_diff {α : Type u} (s : Set α) : ∅ \ s = ∅

theorem Set.diff_eq_empty {α : Type u} {s t : Set α} : s \ t = ∅ ↔ s ⊆ t

@[simp]

theorem Set.diff_empty {α : Type u} {s : Set α} : s \ ∅ = s

@[simp]

theorem Set.diff_univ {α : Type u} (s : Set α) : s \ univ = ∅

theorem Set.diff_diff {α : Type u} {s t u : Set α} : (s \ t) \ u = s \ (t ∪ u)

theorem Set.diff_diff_comm {α : Type u} {s t u : Set α} : (s \ t) \ u = (s \ u) \ t

theorem Set.diff_subset_iff {α : Type u} {s t u : Set α} : s \ t ⊆ u ↔ s ⊆ t ∪ u

theorem Set.subset_diff_union {α : Type u} (s t : Set α) : s ⊆ s \ t ∪ t

theorem Set.diff_union_of_subset {α : Type u} {s t : Set α} (h : t ⊆ s) : s \ t ∪ t = s

theorem Set.diff_subset_comm {α : Type u} {s t u : Set α} : s \ t ⊆ u ↔ s \ u ⊆ t

theorem Set.diff_inter {α : Type u} {s t u : Set α} : s \ (t ∩ u) = s \ t ∪ s \ u

theorem Set.diff_inter_diff {α : Type u} {s t u : Set α} : s \ t ∩ (s \ u) = s \ (t ∪ u)

theorem Set.diff_compl {α : Type u} {s t : Set α} : s \ tᶜ = s ∩ t

theorem Set.compl_diff {α : Type u} {s t : Set α} : (t \ s)ᶜ = s ∪ tᶜ

theorem Set.diff_diff_right {α : Type u} {s t u : Set α} : s \ (t \ u) = s \ t ∪ s ∩ u

theorem Set.inter_diff_right_comm {α : Type u} {s t u : Set α} : (s ∩ t) \ u = s \ u ∩ t

theorem Set.diff_inter_right_comm {α : Type u} {s t u : Set α} : s \ u ∩ t = (s ∩ t) \ u

@[simp]

theorem Set.union_diff_self {α : Type u} {s t : Set α} : s ∪ t \ s = s ∪ t

@[simp]

theorem Set.diff_union_self {α : Type u} {s t : Set α} : s \ t ∪ t = s ∪ t

@[simp]

theorem Set.diff_inter_self {α : Type u} {a b : Set α} : b \ a ∩ a = ∅

@[simp]

theorem Set.diff_inter_self_eq_diff {α : Type u} {s t : Set α} : s \ (t ∩ s) = s \ t

@[simp]

theorem Set.diff_self_inter {α : Type u} {s t : Set α} : s \ (s ∩ t) = s \ t

theorem Set.diff_self {α : Type u} {s : Set α} : s \ s = ∅

theorem Set.diff_diff_right_self {α : Type u} (s t : Set α) : s \ (s \ t) = s ∩ t

theorem Set.diff_diff_cancel_left {α : Type u} {s t : Set α} (h : s ⊆ t) : t \ (t \ s) = s

theorem Set.union_eq_diff_union_diff_union_inter {α : Type u} (s t : Set α) : s ∪ t = s \ t ∪ t \ s ∪ s ∩ t

Powerset

theorem Set.mem_powerset {α : Type u} {x s : Set α} (h : x ⊆ s) : x ∈ 𝒫 s

theorem Set.subset_of_mem_powerset {α : Type u} {x s : Set α} (h : x ∈ 𝒫 s) : x ⊆ s

@[simp]

theorem Set.mem_powerset_iff {α : Type u} (x s : Set α) : x ∈ 𝒫 s ↔ x ⊆ s

theorem Set.powerset_inter {α : Type u} (s t : Set α) : 𝒫(s ∩ t) = 𝒫 s ∩ 𝒫 t

@[simp]

theorem Set.powerset_mono {α : Type u} {s t : Set α} : 𝒫 s ⊆ 𝒫 t ↔ s ⊆ t

theorem Set.monotone_powerset {α : Type u} : Monotone powerset

@[simp]

theorem Set.powerset_nonempty {α : Type u} {s : Set α} : (𝒫 s).Nonempty

@[simp]

theorem Set.powerset_empty {α : Type u} : 𝒫∅ = {∅}

@[simp]

theorem Set.powerset_univ {α : Type u} : 𝒫 univ = univ

Sets defined as an if-then-else

@[deprecated mem_dite (since := "2025-01-30")]

theorem Set.mem_dite {α : Type u} (p : Prop) [Decidable p] (s : p → Set α) (t : ¬p → Set α) (x : α) : (x ∈ if h : p then s h else t h) ↔ (∀ (h : p), x ∈ s h) ∧ ∀ (h : ¬p), x ∈ t h

theorem Set.mem_dite_univ_right {α : Type u} (p : Prop) [Decidable p] (t : p → Set α) (x : α) : (x ∈ if h : p then t h else univ) ↔ ∀ (h : p), x ∈ t h

@[simp]

theorem Set.mem_ite_univ_right {α : Type u} (p : Prop) [Decidable p] (t : Set α) (x : α) : (x ∈ if p then t else univ) ↔ p → x ∈ t

theorem Set.mem_dite_univ_left {α : Type u} (p : Prop) [Decidable p] (t : ¬p → Set α) (x : α) : (x ∈ if h : p then univ else t h) ↔ ∀ (h : ¬p), x ∈ t h

@[simp]

theorem Set.mem_ite_univ_left {α : Type u} (p : Prop) [Decidable p] (t : Set α) (x : α) : (x ∈ if p then univ else t) ↔ ¬p → x ∈ t

theorem Set.mem_dite_empty_right {α : Type u} (p : Prop) [Decidable p] (t : p → Set α) (x : α) : (x ∈ if h : p then t h else ∅) ↔ ∃ (h : p), x ∈ t h

@[simp]

theorem Set.mem_ite_empty_right {α : Type u} (p : Prop) [Decidable p] (t : Set α) (x : α) : (x ∈ if p then t else ∅) ↔ p ∧ x ∈ t

theorem Set.mem_dite_empty_left {α : Type u} (p : Prop) [Decidable p] (t : ¬p → Set α) (x : α) : (x ∈ if h : p then ∅ else t h) ↔ ∃ (h : ¬p), x ∈ t h

@[simp]

theorem Set.mem_ite_empty_left {α : Type u} (p : Prop) [Decidable p] (t : Set α) (x : α) : (x ∈ if p then ∅ else t) ↔ ¬p ∧ x ∈ t

If-then-else for sets

def Set.ite {α : Type u} (t s s' : Set α) : Set α

ite for sets: Set.ite t s s' ∩ t = s ∩ t, Set.ite t s s' ∩ tᶜ = s' ∩ tᶜ. Defined as s ∩ t ∪ s' \ t.

Equations

• t.ite s s' = s ∩ t ∪ s' \ t

@[simp]

theorem Set.ite_inter_self {α : Type u} (t s s' : Set α) : t.ite s s' ∩ t = s ∩ t

@[simp]

theorem Set.ite_compl {α : Type u} (t s s' : Set α) : tᶜ.ite s s' = t.ite s' s

@[simp]

theorem Set.ite_inter_compl_self {α : Type u} (t s s' : Set α) : t.ite s s' ∩ tᶜ = s' ∩ tᶜ

@[simp]

theorem Set.ite_diff_self {α : Type u} (t s s' : Set α) : t.ite s s' \ t = s' \ t

@[simp]

theorem Set.ite_same {α : Type u} (t s : Set α) : t.ite s s = s

@[simp]

theorem Set.ite_left {α : Type u} (s t : Set α) : s.ite s t = s ∪ t

@[simp]

theorem Set.ite_right {α : Type u} (s t : Set α) : s.ite t s = t ∩ s

@[simp]

theorem Set.ite_empty {α : Type u} (s s' : Set α) : ∅.ite s s' = s'

@[simp]

theorem Set.ite_univ {α : Type u} (s s' : Set α) : univ.ite s s' = s

@[simp]

theorem Set.ite_empty_left {α : Type u} (t s : Set α) : t.ite ∅ s = s \ t

@[simp]

theorem Set.ite_empty_right {α : Type u} (t s : Set α) : t.ite s ∅ = s ∩ t

theorem Set.ite_mono {α : Type u} (t : Set α) {s₁ s₁' s₂ s₂' : Set α} (h : s₁ ⊆ s₂) (h' : s₁' ⊆ s₂') : t.ite s₁ s₁' ⊆ t.ite s₂ s₂'

theorem Set.ite_subset_union {α : Type u} (t s s' : Set α) : t.ite s s' ⊆ s ∪ s'

theorem Set.inter_subset_ite {α : Type u} (t s s' : Set α) : s ∩ s' ⊆ t.ite s s'

theorem Set.ite_inter_inter {α : Type u} (t s₁ s₂ s₁' s₂' : Set α) : t.ite (s₁ ∩ s₂) (s₁' ∩ s₂') = t.ite s₁ s₁' ∩ t.ite s₂ s₂'

theorem Set.ite_inter {α : Type u} (t s₁ s₂ s : Set α) : t.ite (s₁ ∩ s) (s₂ ∩ s) = t.ite s₁ s₂ ∩ s

theorem Set.ite_inter_of_inter_eq {α : Type u} (t : Set α) {s₁ s₂ s : Set α} (h : s₁ ∩ s = s₂ ∩ s) : t.ite s₁ s₂ ∩ s = s₁ ∩ s

theorem Set.subset_ite {α : Type u} {t s s' u : Set α} : u ⊆ t.ite s s' ↔ u ∩ t ⊆ s ∧ u \ t ⊆ s'

theorem Set.ite_eq_of_subset_left {α : Type u} (t : Set α) {s₁ s₂ : Set α} (h : s₁ ⊆ s₂) : t.ite s₁ s₂ = s₁ ∪ s₂ \ t

theorem Set.ite_eq_of_subset_right {α : Type u} (t : Set α) {s₁ s₂ : Set α} (h : s₂ ⊆ s₁) : t.ite s₁ s₂ = s₁ ∩ t ∪ s₂

theorem Function.Injective.nonempty_apply_iff {α : Type u_1} {β : Type u_2} {f : Set α → Set β} (hf : Injective f) (h2 : f ∅ = ∅) {s : Set α} : (f s).Nonempty ↔ s.Nonempty

theorem Subsingleton.eq_univ_of_nonempty {α : Type u_1} [Subsingleton α] {s : Set α} : s.Nonempty → s = Set.univ

theorem Subsingleton.set_cases {α : Type u_1} [Subsingleton α] {p : Set α → Prop} (h0 : p ∅) (h1 : p Set.univ) (s : Set α) : p s

theorem Subsingleton.mem_iff_nonempty {α : Type u_2} [Subsingleton α] {s : Set α} {x : α} : x ∈ s ↔ s.Nonempty

Decidability instances for sets

instance Set.decidableSdiff {α : Type u} (s t : Set α) (a : α) [Decidable (a ∈ s)] [Decidable (a ∈ t)] : Decidable (a ∈ s \ t)

Equations

• s.decidableSdiff t a = inferInstanceAs (Decidable (a ∈ s ∧ a ∉ t))

instance Set.decidableInter {α : Type u} (s t : Set α) (a : α) [Decidable (a ∈ s)] [Decidable (a ∈ t)] : Decidable (a ∈ s ∩ t)

Equations

• s.decidableInter t a = inferInstanceAs (Decidable (a ∈ s ∧ a ∈ t))

instance Set.decidableUnion {α : Type u} (s t : Set α) (a : α) [Decidable (a ∈ s)] [Decidable (a ∈ t)] : Decidable (a ∈ s ∪ t)

Equations

• s.decidableUnion t a = inferInstanceAs (Decidable (a ∈ s ∨ a ∈ t))

instance Set.decidableCompl {α : Type u} (s : Set α) (a : α) [Decidable (a ∈ s)] : Decidable (a ∈ sᶜ)

Equations

• s.decidableCompl a = inferInstanceAs (Decidable (a ∉ s))

instance Set.decidableEmptyset {α : Type u} (a : α) : Decidable (a ∈ ∅)

Equations

• Set.decidableEmptyset a = isFalse ⋯

instance Set.decidableUniv {α : Type u} (a : α) : Decidable (a ∈ univ)

Equations

• Set.decidableUniv a = isTrue ⋯

instance Set.decidableInsert {α : Type u} (s : Set α) (a b : α) [Decidable (a = b)] [Decidable (a ∈ s)] : Decidable (a ∈ insert b s)

Equations

• s.decidableInsert a b = inferInstanceAs (Decidable (a = b ∨ a ∈ s))

instance Set.decidableSetOf {α : Type u} (a : α) (p : α → Prop) [Decidable (p a)] : Decidable (a ∈ {a : α | p a})

Equations

• Set.decidableSetOf a p = inst✝

def Equiv.setSubtypeComm {α : Type u_1} (p : α → Prop) : Set { a : α // p a } ≃ { s : Set α // ∀ a ∈ s, p a }

Given a predicate p : α → Prop, produces an equivalence between Set {a : α // p a} and {s : Set α // ∀ a ∈ s, p a}.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Equiv.setSubtypeComm_apply {α : Type u_1} (p : α → Prop) (s : Set { a : α // p a }) : (Equiv.setSubtypeComm p) s = ⟨{a : α | ∃ (h : p a), ⟨a, h⟩ ∈ s}, ⋯⟩

@[simp]

theorem Equiv.setSubtypeComm_symm_apply {α : Type u_1} (p : α → Prop) (s : { s : Set α // ∀ a ∈ s, p a }) : (Equiv.setSubtypeComm p).symm s = {a : { a : α // p a } | ↑a ∈ ↑s}