Documentation

Mathlib.Data.Set.Basic

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 core library.

This file provides some basic definitions related to sets and functions not present in the core library, as well as extra lemmas for functions in the core library (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:

Definitions in the file:

Notation #

Implementation notes #

Tags #

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

Set coercion to a type #

Equations
  • Set.instBooleanAlgebraSet = let __src := inferInstance; BooleanAlgebra.mk
instance Set.instHasSSubset {α : Type u} :
Equations
  • Set.instHasSSubset = { SSubset := fun (x x_1 : Set α) => x < x_1 }
@[simp]
theorem Set.top_eq_univ {α : Type u} :
= Set.univ
@[simp]
theorem Set.bot_eq_empty {α : Type u} :
@[simp]
theorem Set.sup_eq_union {α : Type u} :
(fun (x x_1 : Set α) => x x_1) = fun (x x_1 : Set α) => x x_1
@[simp]
theorem Set.inf_eq_inter {α : Type u} :
(fun (x x_1 : Set α) => x x_1) = fun (x x_1 : Set α) => x x_1
@[simp]
theorem Set.le_eq_subset {α : Type u} :
(fun (x x_1 : Set α) => x x_1) = fun (x x_1 : Set α) => x x_1
@[simp]
theorem Set.lt_eq_ssubset {α : Type u} :
(fun (x x_1 : Set α) => x < x_1) = fun (x x_1 : Set α) => x x_1
theorem Set.le_iff_subset {α : Type u} {s : Set α} {t : Set α} :
s t s t
theorem Set.lt_iff_ssubset {α : Type u} {s : Set α} {t : Set α} :
s < t s t
theorem HasSubset.Subset.le {α : Type u} {s : Set α} {t : Set α} :
s ts t

Alias of the reverse direction of Set.le_iff_subset.

theorem LE.le.subset {α : Type u} {s : Set α} {t : Set α} :
s ts t

Alias of the forward direction of Set.le_iff_subset.

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

Alias of the reverse direction of Set.lt_iff_ssubset.

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

Alias of the forward 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
Equations
  • =
instance Set.PiSetCoe.canLift' (ι : Type u) (α : Type v) [Nonempty α] (s : Set ι) :
CanLift (sα) (ια) (fun (f : ια) (i : s) => f i) fun (x : sα) => True
Equations
  • =
instance instCoeTCElem {α : Type u} (s : Set α) :
CoeTC (s) α
Equations
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 : sProp} :
(∀ (x : s), p x) ∀ (x : α) (h : x s), p x, h
theorem SetCoe.exists {α : Type u} {s : Set α} {p : sProp} :
(∃ (x : s), p x) ∃ (x : α) (h : x s), p x, h
theorem SetCoe.exists' {α : Type u} {s : Set α} {p : (x : α) → x sProp} :
(∃ (x : α) (h : x s), p x h) ∃ (x : s), p x
theorem SetCoe.forall' {α : Type u} {s : Set α} {p : (x : α) → x sProp} :
(∀ (x : α) (h : x s), p x h) ∀ (x : s), p x
@[simp]
theorem set_coe_cast {α : Type u} {s : Set α} {t : Set α} (H' : s = t) (H : s = t) (x : s) :
cast H x = x,
theorem SetCoe.ext {α : Type u} {s : Set α} {a : s} {b : s} :
a = ba = b
theorem SetCoe.ext_iff {α : Type u} {s : Set α} {a : s} {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 : Set α} {t : Set α} :
s = ts t

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

instance Set.instInhabited {α : Type u} :
Equations
  • Set.instInhabited = { default := }
theorem Set.ext_iff {α : Type u} {s : Set α} {t : Set α} :
s = t ∀ (x : α), x s x t
theorem Set.mem_of_mem_of_subset {α : Type u} {x : α} {s : Set α} {t : Set α} (hx : x s) (h : s t) :
x t
theorem Set.forall_in_swap {α : Type u} {β : Type v} {s : Set α} {p : αβProp} :
(as, ∀ (b : β), p a b) ∀ (b : β), as, p a b

Lemmas about mem and setOf #

theorem Set.mem_setOf {α : Type u} {a : α} {p : αProp} :
a {x : α | p x} p a
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.subset_setOf {α : Type u} {p : αProp} {s : Set α} :
s setOf p xs, p x
theorem Set.setOf_subset {α : Type u} {p : αProp} {s : Set α} :
setOf p s ∀ (x : α), p xx s
@[simp]
theorem Set.setOf_subset_setOf {α : Type u} {p : αProp} {q : αProp} :
{a : α | p a} {a : α | q a} ∀ (a : α), p aq a
theorem Set.setOf_and {α : Type u} {p : αProp} {q : αProp} :
{a : α | p a q a} = {a : α | p a} {a : α | q a}
theorem Set.setOf_or {α : Type u} {p : αProp} {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 (x x_1 : Set α) => x x_1
Equations
  • =
instance Set.instIsTransSubset {α : Type u} :
IsTrans (Set α) fun (x x_1 : Set α) => x x_1
Equations
  • =
instance Set.instTransSubset {α : Type u} :
Trans (fun (x x_1 : Set α) => x x_1) (fun (x x_1 : Set α) => x x_1) fun (x x_1 : Set α) => x x_1
Equations
  • Set.instTransSubset = let_fun this := inferInstance; this
instance Set.instIsAntisymmSubset {α : Type u} :
IsAntisymm (Set α) fun (x x_1 : Set α) => x x_1
Equations
  • =
instance Set.instIsIrreflSSubset {α : Type u} :
IsIrrefl (Set α) fun (x x_1 : Set α) => x x_1
Equations
  • =
instance Set.instIsTransSSubset {α : Type u} :
IsTrans (Set α) fun (x x_1 : Set α) => x x_1
Equations
  • =
instance Set.instTransSSubset {α : Type u} :
Trans (fun (x x_1 : Set α) => x x_1) (fun (x x_1 : Set α) => x x_1) fun (x x_1 : Set α) => x x_1
Equations
  • Set.instTransSSubset = let_fun this := inferInstance; this
instance Set.instTransSSubsetSubset {α : Type u} :
Trans (fun (x x_1 : Set α) => x x_1) (fun (x x_1 : Set α) => x x_1) fun (x x_1 : Set α) => x x_1
Equations
  • Set.instTransSSubsetSubset = let_fun this := inferInstance; this
instance Set.instTransSubsetSSubset {α : Type u} :
Trans (fun (x x_1 : Set α) => x x_1) (fun (x x_1 : Set α) => x x_1) fun (x x_1 : Set α) => x x_1
Equations
  • Set.instTransSubsetSSubset = let_fun this := inferInstance; this
instance Set.instIsAsymmSSubset {α : Type u} :
IsAsymm (Set α) fun (x x_1 : Set α) => x x_1
Equations
  • =
instance Set.instIsNonstrictStrictOrderSubsetSSubset {α : Type u} :
IsNonstrictStrictOrder (Set α) (fun (x x_1 : Set α) => x x_1) fun (x x_1 : Set α) => x x_1
Equations
  • =
theorem Set.subset_def {α : Type u} {s : Set α} {t : Set α} :
(s t) = xs, x t
theorem Set.ssubset_def {α : Type u} {s : Set α} {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 : Set α} {b : Set α} {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 : Set α} {b : Set α} (h₁ : a b) (h₂ : b a) :
a = b
theorem Set.Subset.antisymm_iff {α : Type u} {a : Set α} {b : Set α} :
a = b a b b a
theorem Set.eq_of_subset_of_subset {α : Type u} {a : Set α} {b : Set α} :
a bb aa = b
theorem Set.mem_of_subset_of_mem {α : Type u} {s₁ : Set α} {s₂ : Set α} {a : α} (h : s₁ s₂) :
a s₁a s₂
theorem Set.not_mem_subset {α : Type u} {a : α} {s : Set α} {t : Set α} (h : s t) :
atas
theorem Set.not_subset {α : Type u} {s : Set α} {t : Set α} :
¬s t as, at
theorem Set.eq_of_forall_subset_iff {α : Type u} {s : Set α} {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 : Set α} {t : Set α} (h : s t) :
s = t s t
theorem Set.exists_of_ssubset {α : Type u} {s : Set α} {t : Set α} (h : s t) :
xt, xs
theorem Set.ssubset_iff_subset_ne {α : Type u} {s : Set α} {t : Set α} :
s t s t s t
theorem Set.ssubset_iff_of_subset {α : Type u} {s : Set α} {t : Set α} (h : s t) :
s t xt, xs
theorem Set.ssubset_of_ssubset_of_subset {α : Type u} {s₁ : Set α} {s₂ : Set α} {s₃ : Set α} (hs₁s₂ : s₁ s₂) (hs₂s₃ : s₂ s₃) :
s₁ s₃
theorem Set.ssubset_of_subset_of_ssubset {α : Type u} {s₁ : Set α} {s₂ : Set α} {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 α} :
¬as 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.NonemptyNonempty 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
Instances For
    theorem Set.Nonempty.some_mem {α : Type u} {s : Set α} (h : s.Nonempty) :
    h.some s
    theorem Set.Nonempty.mono {α : Type u} {s : Set α} {t : Set α} (ht : s t) (hs : s.Nonempty) :
    t.Nonempty
    theorem Set.nonempty_of_not_subset {α : Type u} {s : Set α} {t : Set α} (h : ¬s t) :
    (s \ t).Nonempty
    theorem Set.nonempty_of_ssubset {α : Type u} {s : Set α} {t : Set α} (ht : s t) :
    (t \ s).Nonempty
    theorem Set.Nonempty.of_diff {α : Type u} {s : Set α} {t : Set α} (h : (s \ t).Nonempty) :
    s.Nonempty
    theorem Set.nonempty_of_ssubset' {α : Type u} {s : Set α} {t : Set α} (ht : s t) :
    t.Nonempty
    theorem Set.Nonempty.inl {α : Type u} {s : Set α} {t : Set α} (hs : s.Nonempty) :
    (s t).Nonempty
    theorem Set.Nonempty.inr {α : Type u} {s : Set α} {t : Set α} (ht : t.Nonempty) :
    (s t).Nonempty
    @[simp]
    theorem Set.union_nonempty {α : Type u} {s : Set α} {t : Set α} :
    (s t).Nonempty s.Nonempty t.Nonempty
    theorem Set.Nonempty.left {α : Type u} {s : Set α} {t : Set α} (h : (s t).Nonempty) :
    s.Nonempty
    theorem Set.Nonempty.right {α : Type u} {s : Set α} {t : Set α} (h : (s t).Nonempty) :
    t.Nonempty
    theorem Set.inter_nonempty {α : Type u} {s : Set α} {t : Set α} :
    (s t).Nonempty xs, x t
    theorem Set.inter_nonempty_iff_exists_left {α : Type u} {s : Set α} {t : Set α} :
    (s t).Nonempty xs, x t
    theorem Set.inter_nonempty_iff_exists_right {α : Type u} {s : Set α} {t : Set α} :
    (s t).Nonempty xt, x s
    theorem Set.nonempty_iff_univ_nonempty {α : Type u} :
    Nonempty α Set.univ.Nonempty
    @[simp]
    theorem Set.univ_nonempty {α : Type u} [Nonempty α] :
    Set.univ.Nonempty
    theorem Set.Nonempty.to_subtype {α : Type u} {s : Set α} :
    s.NonemptyNonempty s
    theorem Set.Nonempty.to_type {α : Type u} {s : Set α} :
    s.NonemptyNonempty α
    instance Set.univ.nonempty {α : Type u} [Nonempty α] :
    Nonempty Set.univ
    Equations
    • =
    theorem Set.nonempty_of_nonempty_subtype {α : Type u} {s : Set α} [Nonempty s] :
    s.Nonempty

    Lemmas about the empty set #

    theorem Set.empty_def {α : Type u} :
    = {_x : α | False}
    @[simp]
    theorem Set.mem_empty_iff_false {α : Type u} (x : α) :
    @[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 α) :
    theorem Set.subset_empty_iff {α : Type u} {s : Set α} :
    theorem Set.eq_empty_iff_forall_not_mem {α : Type u} {s : Set α} :
    s = ∀ (x : α), xs
    theorem Set.eq_empty_of_forall_not_mem {α : Type u} {s : Set α} (h : ∀ (x : α), xs) :
    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.Nonempty.ne_empty {α : Type u} {s : Set α} :
    s.Nonemptys

    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
    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 : Set α} {t : Set α} (h : t s) (e : s = ) :
    t =
    theorem Set.forall_mem_empty {α : Type u} {p : αProp} :
    (x, p x) True
    @[deprecated Set.forall_mem_empty]
    theorem Set.ball_empty_iff {α : Type u} {p : αProp} :
    (x, p x) True

    Alias of Set.forall_mem_empty.

    Equations
    • =
    @[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} = Set.univ
    @[simp]
    theorem Set.setOf_top {α : Type u} :
    {_x : α | } = Set.univ
    @[simp]
    theorem Set.univ_eq_empty_iff {α : Type u} :
    Set.univ = IsEmpty α
    theorem Set.empty_ne_univ {α : Type u} [Nonempty α] :
    Set.univ
    @[simp]
    theorem Set.subset_univ {α : Type u} (s : Set α) :
    s Set.univ
    @[simp]
    theorem Set.univ_subset_iff {α : Type u} {s : Set α} :
    Set.univ s s = Set.univ
    theorem Set.eq_univ_of_univ_subset {α : Type u} {s : Set α} :
    Set.univ ss = Set.univ

    Alias of the forward direction of Set.univ_subset_iff.

    theorem Set.eq_univ_iff_forall {α : Type u} {s : Set α} :
    s = Set.univ ∀ (x : α), x s
    theorem Set.eq_univ_of_forall {α : Type u} {s : Set α} :
    (∀ (x : α), x s)s = Set.univ
    theorem Set.Nonempty.eq_univ {α : Type u} {s : Set α} [Subsingleton α] :
    s.Nonemptys = Set.univ
    theorem Set.eq_univ_of_subset {α : Type u} {s : Set α} {t : Set α} (h : s t) (hs : s = Set.univ) :
    t = Set.univ
    theorem Set.exists_mem_of_nonempty (α : Type u_1) [Nonempty α] :
    ∃ (x : α), x Set.univ
    theorem Set.ne_univ_iff_exists_not_mem {α : Type u_1} (s : Set α) :
    s Set.univ ∃ (a : α), as
    theorem Set.not_subset_iff_exists_mem_not_mem {α : Type u_1} {s : Set α} {t : Set α} :
    ¬s t xs, xt
    theorem Set.univ_unique {α : Type u} [Unique α] :
    Set.univ = {default}
    theorem Set.ssubset_univ_iff {α : Type u} {s : Set α} :
    s Set.univ s Set.univ
    Equations
    • =

    Lemmas about union #

    theorem Set.union_def {α : Type u} {s₁ : Set α} {s₂ : Set α} :
    s₁ s₂ = {a : α | a s₁ a s₂}
    theorem Set.mem_union_left {α : Type u} {x : α} {a : Set α} (b : Set α) :
    x ax a b
    theorem Set.mem_union_right {α : Type u} {x : α} {b : Set α} (a : Set α) :
    x bx a b
    theorem Set.mem_or_mem_of_mem_union {α : Type u} {x : α} {a : Set α} {b : Set α} (H : x a b) :
    x a x b
    theorem Set.MemUnion.elim {α : Type u} {x : α} {a : Set α} {b : Set α} {P : Prop} (H₁ : x a b) (H₂ : x aP) (H₃ : x bP) :
    P
    @[simp]
    theorem Set.mem_union {α : Type u} (x : α) (a : Set α) (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 : Set α) (b : Set α) :
    a b = b a
    theorem Set.union_assoc {α : Type u} (a : Set α) (b : Set α) (c : Set α) :
    a b c = a (b c)
    instance Set.union_isAssoc {α : Type u} :
    Std.Associative fun (x x_1 : Set α) => x x_1
    Equations
    • =
    instance Set.union_isComm {α : Type u} :
    Std.Commutative fun (x x_1 : Set α) => x x_1
    Equations
    • =
    theorem Set.union_left_comm {α : Type u} (s₁ : Set α) (s₂ : Set α) (s₃ : Set α) :
    s₁ (s₂ s₃) = s₂ (s₁ s₃)
    theorem Set.union_right_comm {α : Type u} (s₁ : Set α) (s₂ : Set α) (s₃ : Set α) :
    s₁ s₂ s₃ = s₁ s₃ s₂
    @[simp]
    theorem Set.union_eq_left {α : Type u} {s : Set α} {t : Set α} :
    s t = s t s
    @[simp]
    theorem Set.union_eq_right {α : Type u} {s : Set α} {t : Set α} :
    s t = t s t
    theorem Set.union_eq_self_of_subset_left {α : Type u} {s : Set α} {t : Set α} (h : s t) :
    s t = t
    theorem Set.union_eq_self_of_subset_right {α : Type u} {s : Set α} {t : Set α} (h : t s) :
    s t = s
    @[simp]
    theorem Set.subset_union_left {α : Type u} {s : Set α} {t : Set α} :
    s s t
    @[simp]
    theorem Set.subset_union_right {α : Type u} {s : Set α} {t : Set α} :
    t s t
    theorem Set.union_subset {α : Type u} {s : Set α} {t : Set α} {r : Set α} (sr : s r) (tr : t r) :
    s t r
    @[simp]
    theorem Set.union_subset_iff {α : Type u} {s : Set α} {t : Set α} {u : Set α} :
    s t u s u t u
    theorem Set.union_subset_union {α : Type u} {s₁ : Set α} {s₂ : Set α} {t₁ : Set α} {t₂ : Set α} (h₁ : s₁ s₂) (h₂ : t₁ t₂) :
    s₁ t₁ s₂ t₂
    theorem Set.union_subset_union_left {α : Type u} {s₁ : Set α} {s₂ : Set α} (t : Set α) (h : s₁ s₂) :
    s₁ t s₂ t
    theorem Set.union_subset_union_right {α : Type u} (s : Set α) {t₁ : Set α} {t₂ : Set α} (h : t₁ t₂) :
    s t₁ s t₂
    theorem Set.subset_union_of_subset_left {α : Type u} {s : Set α} {t : Set α} (h : s t) (u : Set α) :
    s t u
    theorem Set.subset_union_of_subset_right {α : Type u} {s : Set α} {u : Set α} (h : s u) (t : Set α) :
    s t u
    theorem Set.union_congr_left {α : Type u} {s : Set α} {t : Set α} {u : Set α} (ht : t s u) (hu : u s t) :
    s t = s u
    theorem Set.union_congr_right {α : Type u} {s : Set α} {t : Set α} {u : Set α} (hs : s t u) (ht : t s u) :
    s u = t u
    theorem Set.union_eq_union_iff_left {α : Type u} {s : Set α} {t : Set α} {u : Set α} :
    s t = s u t s u u s t
    theorem Set.union_eq_union_iff_right {α : Type u} {s : Set α} {t : Set α} {u : Set α} :
    s u = t u s t u t s u
    @[simp]
    theorem Set.union_empty_iff {α : Type u} {s : Set α} {t : Set α} :
    s t = s = t =
    @[simp]
    theorem Set.union_univ {α : Type u} (s : Set α) :
    s Set.univ = Set.univ
    @[simp]
    theorem Set.univ_union {α : Type u} (s : Set α) :
    Set.univ s = Set.univ

    Lemmas about intersection #

    theorem Set.inter_def {α : Type u} {s₁ : Set α} {s₂ : Set α} :
    s₁ s₂ = {a : α | a s₁ a s₂}
    @[simp]
    theorem Set.mem_inter_iff {α : Type u} (x : α) (a : Set α) (b : Set α) :
    x a b x a x b
    theorem Set.mem_inter {α : Type u} {x : α} {a : Set α} {b : Set α} (ha : x a) (hb : x b) :
    x a b
    theorem Set.mem_of_mem_inter_left {α : Type u} {x : α} {a : Set α} {b : Set α} (h : x a b) :
    x a
    theorem Set.mem_of_mem_inter_right {α : Type u} {x : α} {a : Set α} {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 α) :
    @[simp]
    theorem Set.empty_inter {α : Type u} (a : Set α) :
    theorem Set.inter_comm {α : Type u} (a : Set α) (b : Set α) :
    a b = b a
    theorem Set.inter_assoc {α : Type u} (a : Set α) (b : Set α) (c : Set α) :
    a b c = a (b c)
    instance Set.inter_isAssoc {α : Type u} :
    Std.Associative fun (x x_1 : Set α) => x x_1
    Equations
    • =
    instance Set.inter_isComm {α : Type u} :
    Std.Commutative fun (x x_1 : Set α) => x x_1
    Equations
    • =
    theorem Set.inter_left_comm {α : Type u} (s₁ : Set α) (s₂ : Set α) (s₃ : Set α) :
    s₁ (s₂ s₃) = s₂ (s₁ s₃)
    theorem Set.inter_right_comm {α : Type u} (s₁ : Set α) (s₂ : Set α) (s₃ : Set α) :
    s₁ s₂ s₃ = s₁ s₃ s₂
    @[simp]
    theorem Set.inter_subset_left {α : Type u} {s : Set α} {t : Set α} :
    s t s
    @[simp]
    theorem Set.inter_subset_right {α : Type u} {s : Set α} {t : Set α} :
    s t t
    theorem Set.subset_inter {α : Type u} {s : Set α} {t : Set α} {r : Set α} (rs : r s) (rt : r t) :
    r s t
    @[simp]
    theorem Set.subset_inter_iff {α : Type u} {s : Set α} {t : Set α} {r : Set α} :
    r s t r s r t
    @[simp]
    theorem Set.inter_eq_left {α : Type u} {s : Set α} {t : Set α} :
    s t = s s t
    @[simp]
    theorem Set.inter_eq_right {α : Type u} {s : Set α} {t : Set α} :
    s t = t t s
    @[simp]
    theorem Set.left_eq_inter {α : Type u} {s : Set α} {t : Set α} :
    s = s t s t
    @[simp]
    theorem Set.right_eq_inter {α : Type u} {s : Set α} {t : Set α} :
    t = s t t s
    theorem Set.inter_eq_self_of_subset_left {α : Type u} {s : Set α} {t : Set α} :
    s ts t = s
    theorem Set.inter_eq_self_of_subset_right {α : Type u} {s : Set α} {t : Set α} :
    t ss t = t
    theorem Set.inter_congr_left {α : Type u} {s : Set α} {t : Set α} {u : Set α} (ht : s u t) (hu : s t u) :
    s t = s u
    theorem Set.inter_congr_right {α : Type u} {s : Set α} {t : Set α} {u : Set α} (hs : t u s) (ht : s u t) :
    s u = t u
    theorem Set.inter_eq_inter_iff_left {α : Type u} {s : Set α} {t : Set α} {u : Set α} :
    s t = s u s u t s t u
    theorem Set.inter_eq_inter_iff_right {α : Type u} {s : Set α} {t : Set α} {u : Set α} :
    s u = t u t u s s u t
    @[simp]
    theorem Set.inter_univ {α : Type u} (a : Set α) :
    a Set.univ = a
    @[simp]
    theorem Set.univ_inter {α : Type u} (a : Set α) :
    Set.univ a = a
    theorem Set.inter_subset_inter {α : Type u} {s₁ : Set α} {s₂ : Set α} {t₁ : Set α} {t₂ : Set α} (h₁ : s₁ t₁) (h₂ : s₂ t₂) :
    s₁ s₂ t₁ t₂
    theorem Set.inter_subset_inter_left {α : Type u} {s : Set α} {t : Set α} (u : Set α) (H : s t) :
    s u t u
    theorem Set.inter_subset_inter_right {α : Type u} {s : Set α} {t : Set α} (u : Set α) (H : s t) :
    u s u t
    theorem Set.union_inter_cancel_left {α : Type u} {s : Set α} {t : Set α} :
    (s t) s = s
    theorem Set.union_inter_cancel_right {α : Type u} {s : Set α} {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}

    Distributivity laws #

    theorem Set.inter_union_distrib_left {α : Type u} (s : Set α) (t : Set α) (u : Set α) :
    s (t u) = s t s u
    theorem Set.union_inter_distrib_right {α : Type u} (s : Set α) (t : Set α) (u : Set α) :
    (s t) u = s u t u
    theorem Set.union_inter_distrib_left {α : Type u} (s : Set α) (t : Set α) (u : Set α) :
    s t u = (s t) (s u)
    theorem Set.inter_union_distrib_right {α : Type u} (s : Set α) (t : Set α) (u : Set α) :
    s t u = (s u) (t u)
    @[deprecated Set.inter_union_distrib_left]
    theorem Set.inter_distrib_left {α : Type u} (s : Set α) (t : Set α) (u : Set α) :
    s (t u) = s t s u

    Alias of Set.inter_union_distrib_left.

    @[deprecated Set.union_inter_distrib_right]
    theorem Set.inter_distrib_right {α : Type u} (s : Set α) (t : Set α) (u : Set α) :
    (s t) u = s u t u

    Alias of Set.union_inter_distrib_right.

    @[deprecated Set.union_inter_distrib_left]
    theorem Set.union_distrib_left {α : Type u} (s : Set α) (t : Set α) (u : Set α) :
    s t u = (s t) (s u)

    Alias of Set.union_inter_distrib_left.

    @[deprecated Set.inter_union_distrib_right]
    theorem Set.union_distrib_right {α : Type u} (s : Set α) (t : Set α) (u : Set α) :
    s t u = (s u) (t u)

    Alias of Set.inter_union_distrib_right.

    theorem Set.union_union_distrib_left {α : Type u} (s : Set α) (t : Set α) (u : Set α) :
    s (t u) = s t (s u)
    theorem Set.union_union_distrib_right {α : Type u} (s : Set α) (t : Set α) (u : Set α) :
    s t u = s u (t u)
    theorem Set.inter_inter_distrib_left {α : Type u} (s : Set α) (t : Set α) (u : Set α) :
    s (t u) = s t (s u)
    theorem Set.inter_inter_distrib_right {α : Type u} (s : Set α) (t : Set α) (u : Set α) :
    s t u = s u (t u)
    theorem Set.union_union_union_comm {α : Type u} (s : Set α) (t : Set α) (u : Set α) (v : Set α) :
    s t (u v) = s u (t v)
    theorem Set.inter_inter_inter_comm {α : Type u} (s : Set α) (t : Set α) (u : Set α) (v : Set α) :
    s t (u v) = s u (t v)

    Lemmas about insert #

    insert α s is the set {α} ∪ s.

    theorem Set.insert_def {α : Type u} (x : α) (s : Set α) :
    insert x s = {y : α | y = x y s}
    @[simp]
    theorem Set.subset_insert {α : Type u} (x : α) (s : Set α) :
    s insert x s
    theorem Set.mem_insert {α : Type u} (x : α) (s : Set α) :
    x insert x s
    theorem Set.mem_insert_of_mem {α : Type u} {x : α} {s : Set α} (y : α) :
    x sx insert y s
    theorem Set.eq_or_mem_of_mem_insert {α : Type u} {x : α} {a : α} {s : Set α} :
    x insert a sx = a x s
    theorem Set.mem_of_mem_insert_of_ne {α : Type u} {a : α} {b : α} {s : Set α} :
    b insert a sb ab s
    theorem Set.eq_of_not_mem_of_mem_insert {α : Type u} {a : α} {b : α} {s : Set α} :
    b insert a sbsb = a
    @[simp]
    theorem Set.mem_insert_iff {α : Type u} {x : α} {a : α} {s : Set α} :
    x insert a s x = a x s
    @[simp]
    theorem Set.insert_eq_of_mem {α : Type u} {a : α} {s : Set α} (h : a s) :
    insert a s = s
    theorem Set.ne_insert_of_not_mem {α : Type u} {s : Set α} (t : Set α) {a : α} :
    ass insert a t
    @[simp]
    theorem Set.insert_eq_self {α : Type u} {a : α} {s : Set α} :
    insert a s = s a s
    theorem Set.insert_ne_self {α : Type u} {a : α} {s : Set α} :
    insert a s s as
    theorem Set.insert_subset_iff {α : Type u} {a : α} {s : Set α} {t : Set α} :
    insert a s t a t s t
    theorem Set.insert_subset {α : Type u} {a : α} {s : Set α} {t : Set α} (ha : a t) (hs : s t) :
    insert a s t
    theorem Set.insert_subset_insert {α : Type u} {a : α} {s : Set α} {t : Set α} (h : s t) :
    insert a s insert a t
    @[simp]
    theorem Set.insert_subset_insert_iff {α : Type u} {a : α} {s : Set α} {t : Set α} (ha : as) :
    insert a s insert a t s t
    theorem Set.subset_insert_iff_of_not_mem {α : Type u} {a : α} {s : Set α} {t : Set α} (ha : as) :
    s insert a t s t
    theorem Set.ssubset_iff_insert {α : Type u} {s : Set α} {t : Set α} :
    s t as, insert a s t
    theorem Set.ssubset_insert {α : Type u} {s : Set α} {a : α} (h : as) :
    s insert a s
    theorem Set.insert_comm {α : Type u} (a : α) (b : α) (s : Set α) :
    insert a (insert b s) = insert b (insert a s)
    theorem Set.insert_idem {α : Type u} (a : α) (s : Set α) :
    insert a (insert a s) = insert a s
    theorem Set.insert_union {α : Type u} {a : α} {s : Set α} {t : Set α} :
    insert a s t = insert a (s t)
    @[simp]
    theorem Set.union_insert {α : Type u} {a : α} {s : Set α} {t : Set α} :
    s insert a t = insert a (s t)
    @[simp]
    theorem Set.insert_nonempty {α : Type u} (a : α) (s : Set α) :
    (insert a s).Nonempty
    instance Set.instNonemptyElemInsert {α : Type u} (a : α) (s : Set α) :
    Nonempty (insert a s)
    Equations
    • =
    theorem Set.insert_inter_distrib {α : Type u} (a : α) (s : Set α) (t : Set α) :
    insert a (s t) = insert a s insert a t
    theorem Set.insert_union_distrib {α : Type u} (a : α) (s : Set α) (t : Set α) :
    insert a (s t) = insert a s insert a t
    theorem Set.insert_inj {α : Type u} {a : α} {b : α} {s : Set α} (ha : as) :
    insert a s = insert b s a = b
    theorem Set.forall_of_forall_insert {α : Type u} {P : αProp} {a : α} {s : Set α} (H : xinsert a s, P x) (x : α) (h : x s) :
    P x
    theorem Set.forall_insert_of_forall {α : Type u} {P : αProp} {a : α} {s : Set α} (H : xs, P x) (ha : P a) (x : α) (h : x insert a s) :
    P x
    theorem Set.exists_mem_insert {α : Type u} {P : αProp} {a : α} {s : Set α} :
    (xinsert a s, P x) P a xs, P x
    @[deprecated Set.exists_mem_insert]
    theorem Set.bex_insert_iff {α : Type u} {P : αProp} {a : α} {s : Set α} :
    (xinsert a s, P x) P a xs, P x

    Alias of Set.exists_mem_insert.

    theorem Set.forall_mem_insert {α : Type u} {P : αProp} {a : α} {s : Set α} :
    (xinsert a s, P x) P a xs, P x
    @[deprecated Set.forall_mem_insert]
    theorem Set.ball_insert_iff {α : Type u} {P : αProp} {a : α} {s : Set α} :
    (xinsert a s, P x) P a xs, P x

    Alias of Set.forall_mem_insert.

    Lemmas about singletons #

    instance Set.instLawfulSingleton {α : Type u} :
    Equations
    • =
    theorem Set.singleton_def {α : Type u} (a : α) :
    {a} = insert a
    @[simp]
    theorem Set.mem_singleton_iff {α : Type u} {a : α} {b : α} :
    a {b} a = b
    @[simp]
    theorem Set.setOf_eq_eq_singleton {α : Type u} {a : α} :
    {n : α | n = a} = {a}
    @[simp]
    theorem Set.setOf_eq_eq_singleton' {α : Type u} {a : α} :
    {x : α | a = x} = {a}
    theorem Set.mem_singleton {α : Type u} (a : α) :
    a {a}
    theorem Set.eq_of_mem_singleton {α : Type u} {x : α} {y : α} (h : x {y}) :
    x = y
    @[simp]
    theorem Set.singleton_eq_singleton_iff {α : Type u} {x : α} {y : α} :
    {x} = {y} x = y
    theorem Set.mem_singleton_of_eq {α : Type u} {x : α} {y : α} (H : x = y) :
    x {y}
    theorem Set.insert_eq {α : Type u} (x : α) (s : Set α) :
    insert x s = {x} s
    @[simp]
    theorem Set.singleton_nonempty {α : Type u} (a : α) :
    {a}.Nonempty
    @[simp]
    theorem Set.singleton_ne_empty {α : Type u} (a : α) :
    {a}
    theorem Set.empty_ssubset_singleton {α : Type u} {a : α} :
    {a}
    @[simp]
    theorem Set.singleton_subset_iff {α : Type u} {a : α} {s : Set α} :
    {a} s a s
    theorem Set.singleton_subset_singleton {α : Type u} {a : α} {b : α} :
    {a} {b} a = b
    theorem Set.set_compr_eq_eq_singleton {α : Type u} {a : α} :
    {b : α | b = a} = {a}
    @[simp]
    theorem Set.singleton_union {α : Type u} {a : α} {s : Set α} :
    {a} s = insert a s
    @[simp]
    theorem Set.union_singleton {α : Type u} {a : α} {s : Set α} :
    s {a} = insert a s
    @[simp]
    theorem Set.singleton_inter_nonempty {α : Type u} {a : α} {s : Set α} :
    ({a} s).Nonempty a s
    @[simp]
    theorem Set.inter_singleton_nonempty {α : Type u} {a : α} {s : Set α} :
    (s {a}).Nonempty a s
    @[simp]
    theorem Set.singleton_inter_eq_empty {α : Type u} {a : α} {s : Set α} :
    {a} s = as
    @[simp]
    theorem Set.inter_singleton_eq_empty {α : Type u} {a : α} {s : Set α} :
    s {a} = as
    theorem Set.nmem_singleton_empty {α : Type u} {s : Set α} :
    s{} s.Nonempty
    instance Set.uniqueSingleton {α : Type u} (a : α) :
    Unique {a}
    Equations
    theorem Set.eq_singleton_iff_unique_mem {α : Type u} {a : α} {s : Set α} :
    s = {a} a s xs, x = a
    theorem Set.eq_singleton_iff_nonempty_unique_mem {α : Type u} {a : α} {s : Set α} :
    s = {a} s.Nonempty xs, x = a
    @[simp]
    theorem Set.default_coe_singleton {α : Type u} (x : α) :
    default = x,

    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 : Set α} {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 : αProp} {q : αProp} :
    {x : α | x s p x} = {x : α | x s q x} xs, p x q x
    theorem Set.sep_eq_of_subset {α : Type u} {s : Set α} {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 xs, p x
    @[simp]
    theorem Set.sep_eq_empty_iff_mem_false {α : Type u} {s : Set α} {p : αProp} :
    {x : α | x s p x} = xs, ¬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 Set.univ p x} = {x : α | p x}
    @[simp]
    theorem Set.sep_union {α : Type u} {s : Set α} {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 : Set α} {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 : αProp} {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 : αProp} {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 : αProp} {q : αProp} :
    {x : α | x {y : α | p y} q x} = {x : α | p x q x}
    @[simp]
    theorem Set.subset_singleton_iff {α : Type u_1} {s : Set α} {x : α} :
    s {x} ys, y = x
    theorem Set.subset_singleton_iff_eq {α : Type u} {s : Set α} {x : α} :
    s {x} s = s = {x}
    theorem Set.Nonempty.subset_singleton_iff {α : Type u} {a : α} {s : Set α} (h : s.Nonempty) :
    s {a} s = {a}
    theorem Set.ssubset_singleton_iff {α : Type u} {s : Set α} {x : α} :
    s {x} s =
    theorem Set.eq_empty_of_ssubset_singleton {α : Type u} {s : Set α} {x : α} (hs : s {x}) :
    s =
    theorem Set.eq_of_nonempty_of_subsingleton {α : Type u_1} [Subsingleton α] (s : Set α) (t : Set α) [Nonempty s] [Nonempty t] :
    s = t
    theorem Set.eq_of_nonempty_of_subsingleton' {α : Type u_1} [Subsingleton α] {s : Set α} (t : Set α) (hs : s.Nonempty) [Nonempty t] :
    s = t
    theorem Set.Nonempty.eq_zero {α : Type u} [Subsingleton α] [Zero α] {s : Set α} (h : s.Nonempty) :
    s = {0}
    theorem Set.Nonempty.eq_one {α : Type u} [Subsingleton α] [One α] {s : Set α} (h : s.Nonempty) :
    s = {1}

    Disjointness #

    theorem Set.disjoint_iff {α : Type u} {s : Set α} {t : Set α} :
    theorem Set.disjoint_iff_inter_eq_empty {α : Type u} {s : Set α} {t : Set α} :
    Disjoint s t s t =
    theorem Disjoint.inter_eq {α : Type u} {s : Set α} {t : Set α} :
    Disjoint s ts t =
    theorem Set.disjoint_left {α : Type u} {s : Set α} {t : Set α} :
    Disjoint s t ∀ ⦃a : α⦄, a sat
    theorem Set.disjoint_right {α : Type u} {s : Set α} {t : Set α} :
    Disjoint s t ∀ ⦃a : α⦄, a tas
    theorem Set.not_disjoint_iff {α : Type u} {s : Set α} {t : Set α} :
    ¬Disjoint s t xs, x t
    theorem Set.not_disjoint_iff_nonempty_inter {α : Type u} {s : Set α} {t : Set α} :
    ¬Disjoint s t (s t).Nonempty
    theorem Set.Nonempty.not_disjoint {α : Type u} {s : Set α} {t : Set α} :
    (s t).Nonempty¬Disjoint s t

    Alias of the reverse direction of Set.not_disjoint_iff_nonempty_inter.

    theorem Set.disjoint_or_nonempty_inter {α : Type u} (s : Set α) (t : Set α) :
    Disjoint s t (s t).Nonempty
    theorem Set.disjoint_iff_forall_ne {α : Type u} {s : Set α} {t : Set α} :
    Disjoint s t ∀ ⦃a : α⦄, a s∀ ⦃b : α⦄, b ta b
    theorem Disjoint.ne_of_mem {α : Type u} {s : Set α} {t : Set α} :
    Disjoint s t∀ ⦃a : α⦄, a s∀ ⦃b : α⦄, b ta b

    Alias of the forward direction of Set.disjoint_iff_forall_ne.

    theorem Set.disjoint_of_subset_left {α : Type u} {s : Set α} {t : Set α} {u : Set α} (h : s u) (d : Disjoint u t) :
    theorem Set.disjoint_of_subset_right {α : Type u} {s : Set α} {t : Set α} {u : Set α} (h : t u) (d : Disjoint s u) :
    theorem Set.disjoint_of_subset {α : Type u} {s₁ : Set α} {s₂ : Set α} {t₁ : Set α} {t₂ : Set α} (hs : s₁ s₂) (ht : t₁ t₂) (h : Disjoint s₂ t₂) :
    Disjoint s₁ t₁
    @[simp]
    theorem Set.disjoint_union_left {α : Type u} {s : Set α} {t : Set α} {u : Set α} :
    @[simp]
    theorem Set.disjoint_union_right {α : Type u} {s : Set α} {t : Set α} {u : Set α} :
    @[simp]
    theorem Set.disjoint_empty {α : Type u} (s : Set α) :
    @[simp]
    theorem Set.empty_disjoint {α : Type u} (s : Set α) :
    @[simp]
    theorem Set.univ_disjoint {α : Type u} {s : Set α} :
    Disjoint Set.univ s s =
    @[simp]
    theorem Set.disjoint_univ {α : Type u} {s : Set α} :
    Disjoint s Set.univ s =
    theorem Set.disjoint_sdiff_left {α : Type u} {s : Set α} {t : Set α} :
    Disjoint (t \ s) s
    theorem Set.disjoint_sdiff_right {α : Type u} {s : Set α} {t : Set α} :
    Disjoint s (t \ s)
    theorem Set.disjoint_sdiff_inter {α : Type u} {s : Set α} {t : Set α} :
    Disjoint (s \ t) (s t)
    theorem Set.diff_union_diff_cancel {α : Type u} {s : Set α} {t : Set α} {u : Set α} (hts : t s) (hut : u t) :
    s \ t t \ u = s \ u
    theorem Set.diff_diff_eq_sdiff_union {α : Type u} {s : Set α} {t : Set α} {u : Set α} (h : u s) :
    s \ (t \ u) = s \ t u
    @[simp]
    theorem Set.disjoint_singleton_left {α : Type u} {a : α} {s : Set α} :
    Disjoint {a} s as
    @[simp]
    theorem Set.disjoint_singleton_right {α : Type u} {a : α} {s : Set α} :
    Disjoint s {a} as
    theorem Set.disjoint_singleton {α : Type u} {a : α} {b : α} :
    Disjoint {a} {b} a b
    theorem Set.subset_diff {α : Type u} {s : Set α} {t : Set α} {u : Set α} :
    s t \ u s t Disjoint s u
    theorem Set.ssubset_iff_sdiff_singleton {α : Type u} {s : Set α} {t : Set α} :
    s t at, s t \ {a}
    theorem Set.inter_diff_distrib_left {α : Type u} (s : Set α) (t : Set α) (u : Set α) :
    s (t \ u) = (s t) \ (s u)
    theorem Set.inter_diff_distrib_right {α : Type u} (s : Set α) (t : Set α) (u : Set α) :
    s \ t u = (s u) \ (t u)

    Lemmas about complement #

    theorem Set.compl_def {α : Type u} (s : Set α) :
    s = {x : α | xs}
    theorem Set.mem_compl {α : Type u} {s : Set α} {x : α} (h : xs) :
    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) :
    xs
    theorem Set.not_mem_compl_iff {α : Type u} {s : Set α} {x : α} :
    xs x s
    @[simp]
    theorem Set.inter_compl_self {α : Type u} (s : Set α) :
    @[simp]
    theorem Set.compl_inter_self {α : Type u} (s : Set α) :
    @[simp]
    theorem Set.compl_empty {α : Type u} :
    = Set.univ
    @[simp]
    theorem Set.compl_union {α : Type u} (s : Set α) (t : Set α) :
    (s t) = s t
    theorem Set.compl_inter {α : Type u} (s : Set α) (t : Set α) :
    (s t) = s t
    @[simp]
    theorem Set.compl_univ {α : Type u} :
    Set.univ =
    @[simp]
    theorem Set.compl_empty_iff {α : Type u} {s : Set α} :
    s = s = Set.univ
    @[simp]
    theorem Set.compl_univ_iff {α : Type u} {s : Set α} :
    s = Set.univ s =
    theorem Set.compl_ne_univ {α : Type u} {s : Set α} :
    s Set.univ s.Nonempty
    theorem Set.nonempty_compl {α : Type u} {s : Set α} :
    s.Nonempty s Set.univ
    @[simp]
    theorem Set.nonempty_compl_of_nontrivial {α : Type u} [Nontrivial α] (x : α) :
    {x}.Nonempty
    theorem Set.mem_compl_singleton_iff {α : Type u} {a : α} {x : α} :
    x {a} x a
    theorem Set.compl_singleton_eq {α : Type u} (a : α) :
    {a} = {x : α | x a}
    @[simp]
    theorem Set.compl_ne_eq_singleton {α : Type u} (a : α) :
    {x : α | x a} = {a}
    theorem Set.union_eq_compl_compl_inter_compl {α : Type u} (s : Set α) (t : Set α) :
    s t = (s t)
    theorem Set.inter_eq_compl_compl_union_compl {α : Type u} (s : Set α) (t : Set α) :
    s t = (s t)
    @[simp]
    theorem Set.union_compl_self {α : Type u} (s : Set α) :
    s s = Set.univ
    @[simp]
    theorem Set.compl_union_self {α : Type u} (s : Set α) :
    s s = Set.univ
    theorem Set.compl_subset_comm {α : Type u} {s : Set α} {t : Set α} :
    s t t s
    theorem Set.subset_compl_comm {α : Type u} {s : Set α} {t : Set α} :
    s t t s
    @[simp]
    theorem Set.compl_subset_compl {α : Type u} {s : Set α} {t : Set α} :
    s t t s
    theorem Set.compl_subset_compl_of_subset {α : Type u} {s : Set α} {t : Set α} (h : t s) :
    theorem Set.subset_compl_iff_disjoint_left {α : Type u} {s : Set α} {t : Set α} :
    theorem Set.subset_compl_iff_disjoint_right {α : Type u} {s : Set α} {t : Set α} :
    theorem Set.disjoint_compl_left_iff_subset {α : Type u} {s : Set α} {t : Set α} :
    theorem Set.disjoint_compl_right_iff_subset {α : Type u} {s : Set α} {t : Set α} :
    theorem Disjoint.subset_compl_right {α : Type u} {s : Set α} {t : Set α} :
    Disjoint s ts t

    Alias of the reverse direction of Set.subset_compl_iff_disjoint_right.

    theorem Disjoint.subset_compl_left {α : Type u} {s : Set α} {t : Set α} :
    Disjoint t ss t

    Alias of the reverse direction of Set.subset_compl_iff_disjoint_left.

    theorem HasSubset.Subset.disjoint_compl_left {α : Type u} {s : Set α} {t : Set α} :
    t sDisjoint s t

    Alias of the reverse direction of Set.disjoint_compl_left_iff_subset.

    theorem HasSubset.Subset.disjoint_compl_right {α : Type u} {s : Set α} {t : Set α} :
    s tDisjoint s t

    Alias of the reverse direction of Set.disjoint_compl_right_iff_subset.

    theorem Set.subset_union_compl_iff_inter_subset {α : Type u} {s : Set α} {t : Set α} {u : Set α} :
    s t u s u t
    theorem Set.compl_subset_iff_union {α : Type u} {s : Set α} {t : Set α} :
    s t s t = Set.univ
    @[simp]
    theorem Set.subset_compl_singleton_iff {α : Type u} {a : α} {s : Set α} :
    s {a} as
    theorem Set.inter_subset {α : Type u} (a : Set α) (b : Set α) (c : Set α) :
    a b c a b c
    theorem Set.inter_compl_nonempty_iff {α : Type u} {s : Set α} {t : Set α} :
    (s t).Nonempty ¬s t

    Lemmas about set difference #

    theorem Set.not_mem_diff_of_mem {α : Type u} {s : Set α} {t : Set α} {x : α} (hx : x t) :
    xs \ t
    theorem Set.mem_of_mem_diff {α : Type u} {s : Set α} {t : Set α} {x : α} (h : x s \ t) :
    x s
    theorem Set.not_mem_of_mem_diff {α : Type u} {s : Set α} {t : Set α} {x : α} (h : x s \ t) :
    xt
    theorem Set.diff_eq_compl_inter {α : Type u} {s : Set α} {t : Set α} :
    s \ t = t s
    theorem Set.nonempty_diff {α : Type u} {s : Set α} {t : Set α} :
    (s \ t).Nonempty ¬s t
    theorem Set.diff_subset {α : Type u} {s : Set α} {t : Set α} :
    s \ t s
    theorem Set.diff_subset_compl {α : Type u} (s : Set α) (t : Set α) :
    s \ t t
    theorem Set.union_diff_cancel' {α : Type u} {s : Set α} {t : Set α} {u : Set α} (h₁ : s t) (h₂ : t u) :
    t u \ s = u
    theorem Set.union_diff_cancel {α : Type u} {s : Set α} {t : Set α} (h : s t) :
    s t \ s = t
    theorem Set.union_diff_cancel_left {α : Type u} {s : Set α} {t : Set α} (h : s t ) :
    (s t) \ s = t
    theorem Set.union_diff_cancel_right {α : Type u} {s : Set α} {t : Set α} (h : s t ) :
    (s t) \ t = s
    @[simp]
    theorem Set.union_diff_left {α : Type u} {s : Set α} {t : Set α} :
    (s t) \ s = t \ s
    @[simp]
    theorem Set.union_diff_right {α : Type u} {s : Set α} {t : Set α} :
    (s t) \ t = s \ t
    theorem Set.union_diff_distrib {α : Type u} {s : Set α} {t : Set α} {u : Set α} :
    (s t) \ u = s \ u t \ u
    theorem Set.inter_diff_assoc {α : Type u} (a : Set α) (b : Set α) (c : Set α) :
    (a b) \ c = a (b \ c)
    @[simp]
    theorem Set.inter_diff_self {α : Type u} (a : Set α) (b : Set α) :
    a (b \ a) =
    @[simp]
    theorem Set.inter_union_diff {α : Type u} (s : Set α) (t : Set α) :
    s t s \ t = s
    @[simp]
    theorem Set.diff_union_inter {α : Type u} (s : Set α) (t : Set α) :
    s \ t s t = s
    @[simp]
    theorem Set.inter_union_compl {α : Type u} (s : Set α) (t : Set α) :
    s t s t = s
    theorem Set.diff_subset_diff {α : Type u} {s₁ : Set α} {s₂ : Set α} {t₁ : Set α} {t₂ : Set α} :
    s₁ s₂t₂ t₁s₁ \ t₁ s₂ \ t₂
    theorem Set.diff_subset_diff_left {α : Type u} {s₁ : Set α} {s₂ : Set α} {t : Set α} (h : s₁ s₂) :
    s₁ \ t s₂ \ t
    theorem Set.diff_subset_diff_right {α : Type u} {s : Set α} {t : Set α} {u : Set α} (h : t u) :
    s \ u s \ t
    theorem Set.compl_eq_univ_diff {α : Type u} (s : Set α) :
    s = Set.univ \ s
    @[simp]
    theorem Set.empty_diff {α : Type u} (s : Set α) :
    theorem Set.diff_eq_empty {α : Type u} {s : Set α} {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 \ Set.univ =
    theorem Set.diff_diff {α : Type u} {s : Set α} {t : Set α} {u : Set α} :
    (s \ t) \ u = s \ (t u)
    theorem Set.diff_diff_comm {α : Type u} {s : Set α} {t : Set α} {u : Set α} :
    (s \ t) \ u = (s \ u) \ t
    theorem Set.diff_subset_iff {α : Type u} {s : Set α} {t : Set α} {u : Set α} :
    s \ t u s t u
    theorem Set.subset_diff_union {α : Type u} (s : Set α) (t : Set α) :
    s s \ t t
    theorem Set.diff_union_of_subset {α : Type u} {s : Set α} {t : Set α} (h : t s) :
    s \ t t = s
    @[simp]
    theorem Set.diff_singleton_subset_iff {α : Type u} {x : α} {s : Set α} {t : Set α} :
    s \ {x} t s insert x t
    theorem Set.subset_diff_singleton {α : Type u} {x : α} {s : Set α} {t : Set α} (h : s t) (hx : xs) :
    s t \ {x}
    theorem Set.subset_insert_diff_singleton {α : Type u} (x : α) (s : Set α) :
    s insert x (s \ {x})
    theorem Set.diff_subset_comm {α : Type u} {s : Set α} {t : Set α} {u : Set α} :
    s \ t u s \ u t
    theorem Set.diff_inter {α : Type u} {s : Set α} {t : Set α} {u : Set α} :
    s \ (t u) = s \ t s \ u
    theorem Set.diff_inter_diff {α : Type u} {s : Set α} {t : Set α} {u : Set α} :
    s \ t (s \ u) = s \ (t u)
    theorem Set.diff_compl {α : Type u} {s : Set α} {t : Set α} :
    s \ t = s t
    theorem Set.diff_diff_right {α : Type u} {s : Set α} {t : Set α} {u : Set α} :
    s \ (t \ u) = s \ t s u
    @[simp]
    theorem Set.insert_diff_of_mem {α : Type u} {a : α} {t : Set α} (s : Set α) (h : a t) :
    insert a s \ t = s \ t
    theorem Set.insert_diff_of_not_mem {α : Type u} {a : α} {t : Set α} (s : Set α) (h : at) :
    insert a s \ t = insert a (s \ t)
    theorem Set.insert_diff_self_of_not_mem {α : Type u} {a : α} {s : Set α} (h : as) :
    insert a s \ {a} = s
    @[simp]
    theorem Set.insert_diff_eq_singleton {α : Type u} {a : α} {s : Set α} (h : as) :
    insert a s \ s = {a}
    theorem Set.inter_insert_of_mem {α : Type u} {a : α} {s : Set α} {t : Set α} (h : a s) :
    s insert a t = insert a (s t)
    theorem Set.insert_inter_of_mem {α : Type u} {a : α} {s : Set α} {t : Set α} (h : a t) :
    insert a s t = insert a (s t)
    theorem Set.inter_insert_of_not_mem {α : Type u} {a : α} {s : Set α} {t : Set α} (h : as) :
    s insert a t = s t
    theorem Set.insert_inter_of_not_mem {α : Type u} {a : α} {s : Set α} {t : Set α} (h : at) :
    insert a s t = s t
    @[simp]
    theorem Set.union_diff_self {α : Type u} {s : Set α} {t : Set α} :
    s t \ s = s t
    @[simp]
    theorem Set.diff_union_self {α : Type u} {s : Set α} {t : Set α} :
    s \ t t = s t
    @[simp]
    theorem Set.diff_inter_self {α : Type u} {a : Set α} {b : Set α} :
    b \ a a =
    @[simp]
    theorem Set.diff_inter_self_eq_diff {α : Type u} {s : Set α} {t : Set α} :
    s \ (t s) = s \ t
    @[simp]
    theorem Set.diff_self_inter {α : Type u} {s : Set α} {t : Set α} :
    s \ (s t) = s \ t
    @[simp]
    theorem Set.diff_singleton_eq_self {α : Type u} {a : α} {s : Set α} (h : as) :
    s \ {a} = s
    @[simp]
    theorem Set.diff_singleton_sSubset {α : Type u} {s : Set α} {a : α} :
    s \ {a} s a s
    @[simp]
    theorem Set.insert_diff_singleton {α : Type u} {a : α} {s : Set α} :
    insert a (s \ {a}) = insert a s
    theorem Set.insert_diff_singleton_comm {α : Type u} {a : α} {b : α} (hab : a b) (s : Set α) :
    insert a (s \ {b}) = insert a s \ {b}
    theorem Set.diff_self {α : Type u} {s : Set α} :
    s \ s =
    theorem Set.diff_diff_right_self {α : Type u} (s : Set α) (t : Set α) :
    s \ (s \ t) = s t
    theorem Set.diff_diff_cancel_left {α : Type u} {s : Set α} {t : Set α} (h : s t) :
    t \ (t \ s) = s
    theorem Set.mem_diff_singleton {α : Type u} {x : α} {y : α} {s : Set α} :
    x s \ {y} x s x y
    theorem Set.mem_diff_singleton_empty {α : Type u} {s : Set α} {t : Set (Set α)} :
    s t \ {} s t s.Nonempty
    theorem Set.subset_insert_iff {α : Type u} {s : Set α} {t : Set α} {x : α} :
    s insert x t s t x s s \ {x} t
    theorem Set.union_eq_diff_union_diff_union_inter {α : Type u} (s : Set α) (t : Set α) :
    s t = s \ t t \ s s t

    Lemmas about pairs #

    theorem Set.pair_eq_singleton {α : Type u} (a : α) :
    {a, a} = {a}
    theorem Set.pair_comm {α : Type u} (a : α) (b : α) :
    {a, b} = {b, a}
    theorem Set.pair_eq_pair_iff {α : Type u} {x : α} {y : α} {z : α} {w : α} :
    {x, y} = {z, w} x = z y = w x = w y = z
    theorem Set.pair_diff_left {α : Type u} {a : α} {b : α} (hne : a b) :
    {a, b} \ {a} = {b}
    theorem Set.pair_diff_right {α : Type u} {a : α} {b : α} (hne : a b) :
    {a, b} \ {b} = {a}
    theorem Set.pair_subset_iff {α : Type u} {a : α} {b : α} {s : Set α} :
    {a, b} s a s b s
    theorem Set.pair_subset {α : Type u} {a : α} {b : α} {s : Set α} (ha : a s) (hb : b s) :
    {a, b} s
    theorem Set.subset_pair_iff {α : Type u} {a : α} {b : α} {s : Set α} :
    s {a, b} xs, x = a x = b
    theorem Set.subset_pair_iff_eq {α : Type u} {s : Set α} {x : α} {y : α} :
    s {x, y} s = s = {x} s = {y} s = {x, y}
    theorem Set.Nonempty.subset_pair_iff_eq {α : Type u} {a : α} {b : α} {s : Set α} (hs : s.Nonempty) :
    s {a, b} s = {a} s = {b} s = {a, b}

    Symmetric difference #

    theorem Set.mem_symmDiff {α : Type u} {a : α} {s : Set α} {t : Set α} :
    a symmDiff s t a s at a t as
    theorem Set.symmDiff_def {α : Type u} (s : Set α) (t : Set α) :
    symmDiff s t = s \ t t \ s
    theorem Set.symmDiff_subset_union {α : Type u} {s : Set α} {t : Set α} :
    symmDiff s t s t
    @[simp]
    theorem Set.symmDiff_eq_empty {α : Type u} {s : Set α} {t : Set α} :
    symmDiff s t = s = t
    @[simp]
    theorem Set.symmDiff_nonempty {α : Type u} {s : Set α} {t : Set α} :
    (symmDiff s t).Nonempty s t
    theorem Set.inter_symmDiff_distrib_left {α : Type u} (s : Set α) (t : Set α) (u : Set α) :
    s symmDiff t u = symmDiff (s t) (s u)
    theorem Set.inter_symmDiff_distrib_right {α : Type u} (s : Set α) (t : Set α) (u : Set α) :
    symmDiff s t u = symmDiff (s u) (t u)
    theorem Set.subset_symmDiff_union_symmDiff_left {α : Type u} {s : Set α} {t : Set α} {u : Set α} (h : Disjoint s t) :
    theorem Set.subset_symmDiff_union_symmDiff_right {α : Type u} {s : Set α} {t : Set α} {u : Set α} (h : Disjoint t u) :

    Powerset #

    theorem Set.mem_powerset {α : Type u} {x : Set α} {s : Set α} (h : x s) :
    x 𝒫 s
    theorem Set.subset_of_mem_powerset {α : Type u} {x : Set α} {s : Set α} (h : x 𝒫 s) :
    x s
    @[simp]
    theorem Set.mem_powerset_iff {α : Type u} (x : Set α) (s : Set α) :
    x 𝒫 s x s
    theorem Set.powerset_inter {α : Type u} (s : Set α) (t : Set α) :
    𝒫(s t) = 𝒫 s 𝒫 t
    @[simp]
    theorem Set.powerset_mono {α : Type u} {s : Set α} {t : Set α} :
    𝒫 s 𝒫 t s t
    theorem Set.monotone_powerset {α : Type u} :
    Monotone Set.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} :
    𝒫 Set.univ = Set.univ
    theorem Set.powerset_singleton {α : Type u} (x : α) :
    𝒫{x} = {, {x}}

    The powerset of a singleton contains only and the singleton itself.

    Sets defined as an if-then-else #

    theorem Set.mem_dite {α : Type u} (p : Prop) [Decidable p] (s : pSet α) (t : ¬pSet α) (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 : pSet α) (x : α) :
    (x if h : p then t h else Set.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 Set.univ) px t
    theorem Set.mem_dite_univ_left {α : Type u} (p : Prop) [Decidable p] (t : ¬pSet α) (x : α) :
    (x if h : p then Set.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 Set.univ else t) ¬px t
    theorem Set.mem_dite_empty_right {α : Type u} (p : Prop) [Decidable p] (t : pSet α) (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 : ¬pSet α) (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 : Set α) (s : Set α) (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
    Instances For
      @[simp]
      theorem Set.ite_inter_self {α : Type u} (t : Set α) (s : Set α) (s' : Set α) :
      t.ite s s' t = s t
      @[simp]
      theorem Set.ite_compl {α : Type u} (t : Set α) (s : Set α) (s' : Set α) :
      t.ite s s' = t.ite s' s
      @[simp]
      theorem Set.ite_inter_compl_self {α : Type u} (t : Set α) (s : Set α) (s' : Set α) :
      t.ite s s' t = s' t
      @[simp]
      theorem Set.ite_diff_self {α : Type u} (t : Set α) (s : Set α) (s' : Set α) :
      t.ite s s' \ t = s' \ t
      @[simp]
      theorem Set.ite_same {α : Type u} (t : Set α) (s : Set α) :
      t.ite s s = s
      @[simp]
      theorem Set.ite_left {α : Type u} (s : Set α) (t : Set α) :
      s.ite s t = s t
      @[simp]
      theorem Set.ite_right {α : Type u} (s : Set α) (t : Set α) :
      s.ite t s = t s
      @[simp]
      theorem Set.ite_empty {α : Type u} (s : Set α) (s' : Set α) :
      .ite s s' = s'
      @[simp]
      theorem Set.ite_univ {α : Type u} (s : Set α) (s' : Set α) :
      Set.univ.ite s s' = s
      @[simp]
      theorem Set.ite_empty_left {α : Type u} (t : Set α) (s : Set α) :
      t.ite s = s \ t
      @[simp]
      theorem Set.ite_empty_right {α : Type u} (t : Set α) (s : Set α) :
      t.ite s = s t
      theorem Set.ite_mono {α : Type u} (t : Set α) {s₁ : Set α} {s₁' : Set α} {s₂ : Set α} {s₂' : Set α} (h : s₁ s₂) (h' : s₁' s₂') :
      t.ite s₁ s₁' t.ite s₂ s₂'
      theorem Set.ite_subset_union {α : Type u} (t : Set α) (s : Set α) (s' : Set α) :
      t.ite s s' s s'
      theorem Set.inter_subset_ite {α : Type u} (t : Set α) (s : Set α) (s' : Set α) :
      s s' t.ite s s'
      theorem Set.ite_inter_inter {α : Type u} (t : Set α) (s₁ : Set α) (s₂ : Set α) (s₁' : Set α) (s₂' : Set α) :
      t.ite (s₁ s₂) (s₁' s₂') = t.ite s₁ s₁' t.ite s₂ s₂'
      theorem Set.ite_inter {α : Type u} (t : Set α) (s₁ : Set α) (s₂ : Set α) (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₁ : Set α} {s₂ : Set α} {s : Set α} (h : s₁ s = s₂ s) :
      t.ite s₁ s₂ s = s₁ s
      theorem Set.subset_ite {α : Type u} {t : Set α} {s : Set α} {s' : Set α} {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₁ : Set α} {s₂ : Set α} (h : s₁ s₂) :
      t.ite s₁ s₂ = s₁ s₂ \ t
      theorem Set.ite_eq_of_subset_right {α : Type u} (t : Set α) {s₁ : Set α} {s₂ : Set α} (h : s₂ s₁) :
      t.ite s₁ s₂ = s₁ t s₂
      theorem Set.monotoneOn_iff_monotone {α : Type u} {β : Type v} {s : Set α} [Preorder α] [Preorder β] {f : αβ} :
      MonotoneOn f s Monotone fun (a : s) => f a
      theorem Set.antitoneOn_iff_antitone {α : Type u} {β : Type v} {s : Set α} [Preorder α] [Preorder β] {f : αβ} :
      AntitoneOn f s Antitone fun (a : s) => f a
      theorem Set.strictMonoOn_iff_strictMono {α : Type u} {β : Type v} {s : Set α} [Preorder α] [Preorder β] {f : αβ} :
      StrictMonoOn f s StrictMono fun (a : s) => f a
      theorem Set.strictAntiOn_iff_strictAnti {α : Type u} {β : Type v} {s : Set α} [Preorder α] [Preorder β] {f : αβ} :
      StrictAntiOn f s StrictAnti fun (a : s) => f a
      theorem Set.not_monotoneOn_not_antitoneOn_iff_exists_le_le {α : Type u} {β : Type v} {s : Set α} [LinearOrder α] [LinearOrder β] {f : αβ} :
      ¬MonotoneOn f s ¬AntitoneOn f s as, bs, cs, a b b c (f a < f b f c < f b f b < f a f b < f c)

      A function between linear orders which is neither monotone nor antitone makes a dent upright or downright.

      theorem Set.not_monotoneOn_not_antitoneOn_iff_exists_lt_lt {α : Type u} {β : Type v} {s : Set α} [LinearOrder α] [LinearOrder β] {f : αβ} :
      ¬MonotoneOn f s ¬AntitoneOn f s as, bs, cs, a < b b < c (f a < f b f c < f b f b < f a f b < f c)

      A function between linear orders which is neither monotone nor antitone makes a dent upright or downright.

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

      Lemmas about inclusion, the injection of subtypes induced by #

      def Set.inclusion {α : Type u_1} {s : Set α} {t : Set α} (h : s t) :
      st

      inclusion is the "identity" function between two subsets s and t, where s ⊆ t

      Equations
      Instances For
        @[simp]
        theorem Set.inclusion_self {α : Type u_1} {s : Set α} (x : s) :
        theorem Set.inclusion_eq_id {α : Type u_1} {s : Set α} (h : s s) :
        @[simp]
        theorem Set.inclusion_mk {α : Type u_1} {s : Set α} {t : Set α} {h : s t} (a : α) (ha : a s) :
        Set.inclusion h a, ha = a,
        theorem Set.inclusion_right {α : Type u_1} {s : Set α} {t : Set α} (h : s t) (x : t) (m : x s) :
        Set.inclusion h x, m = x
        @[simp]
        theorem Set.inclusion_inclusion {α : Type u_1} {s : Set α} {t : Set α} {u : Set α} (hst : s t) (htu : t u) (x : s) :
        @[simp]
        theorem Set.inclusion_comp_inclusion {α : Type u_2} {s : Set α} {t : Set α} {u : Set α} (hst : s t) (htu : t u) :
        @[simp]
        theorem Set.coe_inclusion {α : Type u_1} {s : Set α} {t : Set α} (h : s t) (x : s) :
        (Set.inclusion h x) = x
        theorem Set.val_comp_inclusion {α : Type u_1} {s : Set α} {t : Set α} (h : s t) :
        Subtype.val Set.inclusion h = Subtype.val
        theorem Set.inclusion_injective {α : Type u_1} {s : Set α} {t : Set α} (h : s t) :
        @[simp]
        theorem Set.inclusion_inj {α : Type u_1} {s : Set α} {t : Set α} (h : s t) {x : s} {y : s} :
        theorem Set.eq_of_inclusion_surjective {α : Type u_1} {s : Set α} {t : Set α} {h : s t} (h_surj : Function.Surjective (Set.inclusion h)) :
        s = t
        @[simp]
        theorem Set.inclusion_le_inclusion {α : Type u_1} [Preorder α] {s : Set α} {t : Set α} (h : s t) {x : s} {y : s} :
        @[simp]
        theorem Set.inclusion_lt_inclusion {α : Type u_1} [Preorder α] {s : Set α} {t : Set α} (h : s t) {x : s} {y : s} :
        theorem Subsingleton.eq_univ_of_nonempty {α : Type u_1} [Subsingleton α] {s : Set α} :
        s.Nonemptys = 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 : Set α) (t : Set α) (a : α) [Decidable (a s)] [Decidable (a t)] :
        Decidable (a s \ t)
        Equations
        • s.decidableSdiff t a = inferInstance
        instance Set.decidableInter {α : Type u} (s : Set α) (t : Set α) (a : α) [Decidable (a s)] [Decidable (a t)] :
        Decidable (a s t)
        Equations
        • s.decidableInter t a = inferInstance
        instance Set.decidableUnion {α : Type u} (s : Set α) (t : Set α) (a : α) [Decidable (a s)] [Decidable (a t)] :
        Decidable (a s t)
        Equations
        • s.decidableUnion t a = inferInstance
        instance Set.decidableCompl {α : Type u} (s : Set α) (a : α) [Decidable (a s)] :
        Equations
        • s.decidableCompl a = inferInstance
        instance Set.decidableEmptyset {α : Type u} :
        DecidablePred fun (x : α) => x
        Equations
        instance Set.decidableUniv {α : Type u} :
        DecidablePred fun (x : α) => x Set.univ
        Equations
        instance Set.decidableSetOf {α : Type u} (a : α) (p : αProp) [Decidable (p a)] :
        Decidable (a {a : α | p a})
        Equations
        instance Set.decidableMemSingleton {α : Type u} {a : α} {b : α} [DecidableEq α] :
        Decidable (a {b})
        Equations

        Monotone lemmas for sets #

        theorem Monotone.inter {α : Type u_1} {β : Type u_2} [Preorder β] {f : βSet α} {g : βSet α} (hf : Monotone f) (hg : Monotone g) :
        Monotone fun (x : β) => f x g x
        theorem MonotoneOn.inter {α : Type u_1} {β : Type u_2} [Preorder β] {f : βSet α} {g : βSet α} {s : Set β} (hf : MonotoneOn f s) (hg : MonotoneOn g s) :
        MonotoneOn (fun (x : β) => f x g x) s
        theorem Antitone.inter {α : Type u_1} {β : Type u_2} [Preorder β] {f : βSet α} {g : βSet α} (hf : Antitone f) (hg : Antitone g) :
        Antitone fun (x : β) => f x g x
        theorem AntitoneOn.inter {α : Type u_1} {β : Type u_2} [Preorder β] {f : βSet α} {g : βSet α} {s : Set β} (hf : AntitoneOn f s) (hg : AntitoneOn g s) :
        AntitoneOn (fun (x : β) => f x g x) s
        theorem Monotone.union {α : Type u_1} {β : Type u_2} [Preorder β] {f : βSet α} {g : βSet α} (hf : Monotone f) (hg : Monotone g) :
        Monotone fun (x : β) => f x g x
        theorem MonotoneOn.union {α : Type u_1} {β : Type u_2} [Preorder β] {f : βSet α} {g : βSet α} {s : Set β} (hf : MonotoneOn f s) (hg : MonotoneOn g s) :
        MonotoneOn (fun (x : β) => f x g x) s
        theorem Antitone.union {α : Type u_1} {β : Type u_2} [Preorder β] {f : βSet α} {g : βSet α} (hf : Antitone f) (hg : Antitone g) :
        Antitone fun (x : β) => f x g x
        theorem AntitoneOn.union {α : Type u_1} {β : Type u_2} [Preorder β] {f : βSet α} {g : βSet α} {s : Set β} (hf : AntitoneOn f s) (hg : AntitoneOn g s) :
        AntitoneOn (fun (x : β) => f x g x) s
        theorem Set.monotone_setOf {α : Type u_1} {β : Type u_2} [Preorder α] {p : αβProp} (hp : ∀ (b : β), Monotone fun (a : α) => p a b) :
        Monotone fun (a : α) => {b : β | p a b}
        theorem Set.antitone_setOf {α : Type u_1} {β : Type u_2} [Preorder α] {p : αβProp} (hp : ∀ (b : β), Antitone fun (a : α) => p a b) :
        Antitone fun (a : α) => {b : β | p a b}
        theorem Set.antitone_bforall {α : Type u_1} {P : αProp} :
        Antitone fun (s : Set α) => xs, P x

        Quantifying over a set is antitone in the set

        Disjoint sets #

        theorem Disjoint.union_left {α : Type u_1} {s : Set α} {t : Set α} {u : Set α} (hs : Disjoint s u) (ht : Disjoint t u) :
        Disjoint (s t) u
        theorem Disjoint.union_right {α : Type u_1} {s : Set α} {t : Set α} {u : Set α} (ht : Disjoint s t) (hu : Disjoint s u) :
        Disjoint s (t u)
        theorem Disjoint.inter_left {α : Type u_1} {s : Set α} {t : Set α} (u : Set α) (h : Disjoint s t) :
        Disjoint (s u) t
        theorem Disjoint.inter_left' {α : Type u_1} {s : Set α} {t : Set α} (u : Set α) (h : Disjoint s t) :
        Disjoint (u s) t
        theorem Disjoint.inter_right {α : Type u_1} {s : Set α} {t : Set α} (u : Set α) (h : Disjoint s t) :
        Disjoint s (t u)
        theorem Disjoint.inter_right' {α : Type u_1} {s : Set α} {t : Set α} (u : Set α) (h : Disjoint s t) :
        Disjoint s (u t)
        theorem Disjoint.subset_left_of_subset_union {α : Type u_1} {s : Set α} {t : Set α} {u : Set α} (h : s t u) (hac : Disjoint s u) :
        s t
        theorem Disjoint.subset_right_of_subset_union {α : Type u_1} {s : Set α} {t : Set α} {u : Set α} (h : s t u) (hab : Disjoint s t) :
        s u
        @[simp]
        theorem Prop.compl_singleton (p : Prop) :
        {p} = {¬p}