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 #

@[simp]
theorem Set.top_eq_univ {α : Type u_1} :
= Set.univ
@[simp]
theorem Set.bot_eq_empty {α : Type u_1} :
@[simp]
theorem Set.sup_eq_union {α : Type u_1} :
(fun x x_1 => x x_1) = fun x x_1 => x x_1
@[simp]
theorem Set.inf_eq_inter {α : Type u_1} :
(fun x x_1 => x x_1) = fun x x_1 => x x_1
@[simp]
theorem Set.le_eq_subset {α : Type u_1} :
(fun x x_1 => x x_1) = fun x x_1 => x x_1
@[simp]
theorem Set.lt_eq_ssubset {α : Type u_1} :
(fun x x_1 => x < x_1) = fun x x_1 => x x_1
theorem Set.le_iff_subset {α : Type u_1} {s : Set α} {t : Set α} :
s t s t
theorem Set.lt_iff_ssubset {α : Type u_1} {s : Set α} {t : Set α} :
s < t s t
theorem LE.le.subset {α : Type u_1} {s : Set α} {t : Set α} :
s ts t

Alias of the forward direction of Set.le_iff_subset.

theorem HasSubset.Subset.le {α : Type u_1} {s : Set α} {t : Set α} :
s ts t

Alias of the reverse direction of Set.le_iff_subset.

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

Alias of the forward direction of Set.lt_iff_ssubset.

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

Alias of the reverse direction of Set.lt_iff_ssubset.

@[reducible]
def Set.Elem {α : Type u} (s : Set α) :

Given the set s, Elem s is the Type of element of s.

Instances For
    instance Set.instCoeSortSetType {α : Type u} :
    CoeSort (Set α) (Type u)

    Coercion from a set to the corresponding subtype.

    instance Set.PiSetCoe.canLift (ι : Type u) (α : ιType v) [∀ (i : ι), Nonempty (α i)] (s : Set ι) :
    CanLift ((i : s) → α i) ((i : ι) → α i) (fun f i => f i) fun x => True
    instance Set.PiSetCoe.canLift' (ι : Type u) (α : Type v) [Nonempty α] (s : Set ι) :
    CanLift (sα) (ια) (fun f i => f i) fun x => True
    instance instCoeTCElem {α : Type u} (s : Set α) :
    CoeTC (s) α
    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 { val := x, property := h }
    theorem SetCoe.exists {α : Type u} {s : Set α} {p : sProp} :
    (x, p x) x h, p { val := x, property := h }
    theorem SetCoe.exists' {α : Type u} {s : Set α} {p : (x : α) → x sProp} :
    (x h, p x h) x, p x (_ : x s)
    theorem SetCoe.forall' {α : Type u} {s : Set α} {p : (x : α) → x sProp} :
    ((x : α) → (h : x s) → p x h) (x : s) → p x (_ : x s)
    @[simp]
    theorem set_coe_cast {α : Type u} {s : Set α} {t : Set α} (H' : s = t) (H : s = t) (x : s) :
    cast H x = { val := x, property := (_ : x t) }
    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.

    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} :
    ((a : α) → a s(b : β) → p a b) (b : β) → (a : α) → a sp a b

    Lemmas about mem and setOf #

    @[simp]
    theorem Set.mem_setOf_eq {α : Type u} {x : α} {p : αProp} :
    (x {y | p y}) = p x
    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 : α} :
    setOf (fun x => p x) x p x
    theorem Set.mem_def {α : Type u} {a : α} {s : Set α} :
    a s s a
    @[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.instIsReflSetSubsetInstHasSubsetSet {α : Type u} :
    IsRefl (Set α) fun x x_1 => x x_1
    instance Set.instIsTransSetSubsetInstHasSubsetSet {α : Type u} :
    IsTrans (Set α) fun x x_1 => x x_1
    instance Set.instTransSetSubsetInstHasSubsetSet {α : Type u} :
    Trans (fun x x_1 => x x_1) (fun x x_1 => x x_1) fun x x_1 => x x_1
    instance Set.instIsAntisymmSetSubsetInstHasSubsetSet {α : Type u} :
    IsAntisymm (Set α) fun x x_1 => x x_1
    instance Set.instIsIrreflSetSSubsetInstHasSSubsetSet {α : Type u} :
    IsIrrefl (Set α) fun x x_1 => x x_1
    instance Set.instIsTransSetSSubsetInstHasSSubsetSet {α : Type u} :
    IsTrans (Set α) fun x x_1 => x x_1
    instance Set.instTransSetSSubsetInstHasSSubsetSet {α : Type u} :
    Trans (fun x x_1 => x x_1) (fun x x_1 => x x_1) fun x x_1 => x x_1
    instance Set.instTransSetSSubsetInstHasSSubsetSetSubsetInstHasSubsetSet {α : Type u} :
    Trans (fun x x_1 => x x_1) (fun x x_1 => x x_1) fun x x_1 => x x_1
    instance Set.instTransSetSubsetInstHasSubsetSetSSubsetInstHasSSubsetSet {α : Type u} :
    Trans (fun x x_1 => x x_1) (fun x x_1 => x x_1) fun x x_1 => x x_1
    instance Set.instIsAsymmSetSSubsetInstHasSSubsetSet {α : Type u} :
    IsAsymm (Set α) fun x x_1 => x x_1
    theorem Set.subset_def {α : Type u} {s : Set α} {t : Set α} :
    (s t) = ∀ (x : α), x sx 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) :
    ¬a t¬a s
    theorem Set.not_subset {α : Type u} {s : Set α} {t : Set α} :
    ¬s t a, a s ¬a 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) :
    x, x t ¬x s
    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 x, x t ¬x s
    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 : α) :
    theorem Set.not_not_mem {α : Type u} {a : α} {s : Set α} :
    ¬¬a s a s

    Non-empty sets #

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

    The property s.Nonempty expresses the fact that the set s is not empty. It should be used in theorem assumptions instead of ∃ x, x ∈ s or s ≠ ∅ as it gives access to a nice API thanks to the dot notation.

    Instances For
      theorem Set.nonempty_coe_sort {α : Type u} {s : Set α} :
      theorem Set.Nonempty.coe_sort {α : Type u} {s : Set α} :

      Alias of the reverse direction of Set.nonempty_coe_sort.

      theorem Set.nonempty_def {α : Type u} {s : Set α} :
      Set.Nonempty s x, x s
      theorem Set.nonempty_of_mem {α : Type u} {s : Set α} {x : α} (h : x s) :
      noncomputable def Set.Nonempty.some {α : Type u} {s : Set α} (h : Set.Nonempty s) :
      α

      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.

      Instances For
        theorem Set.Nonempty.some_mem {α : Type u} {s : Set α} (h : Set.Nonempty s) :
        theorem Set.Nonempty.mono {α : Type u} {s : Set α} {t : Set α} (ht : s t) (hs : Set.Nonempty s) :
        theorem Set.nonempty_of_not_subset {α : Type u} {s : Set α} {t : Set α} (h : ¬s t) :
        theorem Set.nonempty_of_ssubset {α : Type u} {s : Set α} {t : Set α} (ht : s t) :
        theorem Set.Nonempty.of_diff {α : Type u} {s : Set α} {t : Set α} (h : Set.Nonempty (s \ t)) :
        theorem Set.nonempty_of_ssubset' {α : Type u} {s : Set α} {t : Set α} (ht : s t) :
        theorem Set.Nonempty.inl {α : Type u} {s : Set α} {t : Set α} (hs : Set.Nonempty s) :
        theorem Set.Nonempty.inr {α : Type u} {s : Set α} {t : Set α} (ht : Set.Nonempty t) :
        @[simp]
        theorem Set.union_nonempty {α : Type u} {s : Set α} {t : Set α} :
        theorem Set.Nonempty.left {α : Type u} {s : Set α} {t : Set α} (h : Set.Nonempty (s t)) :
        theorem Set.Nonempty.right {α : Type u} {s : Set α} {t : Set α} (h : Set.Nonempty (s t)) :
        theorem Set.inter_nonempty {α : Type u} {s : Set α} {t : Set α} :
        Set.Nonempty (s t) x, x s x t
        theorem Set.inter_nonempty_iff_exists_left {α : Type u} {s : Set α} {t : Set α} :
        Set.Nonempty (s t) x, x s x t
        theorem Set.inter_nonempty_iff_exists_right {α : Type u} {s : Set α} {t : Set α} :
        Set.Nonempty (s t) x, x t x s
        @[simp]
        theorem Set.univ_nonempty {α : Type u} [Nonempty α] :
        Set.Nonempty Set.univ
        theorem Set.Nonempty.to_subtype {α : Type u} {s : Set α} :
        theorem Set.Nonempty.to_type {α : Type u} {s : Set α} :
        instance Set.univ.nonempty {α : Type u} [Nonempty α] :
        Nonempty Set.univ

        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.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 : α), ¬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.

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

        Alias of the forward direction of Set.nonempty_iff_ne_empty.


        See also Set.not_nonempty_iff_eq_empty.

        theorem Set.isEmpty_coe_sort {α : Type u} {s : Set α} :
        IsEmpty s s =
        theorem Set.subset_eq_empty {α : Type u} {s : Set α} {t : Set α} (h : t s) (e : s = ) :
        t =
        theorem Set.ball_empty_iff {α : Type u} {p : αProp} :
        ((x : α) → x p x) True
        @[simp]
        theorem Set.empty_ssubset {α : Type u} {s : Set α} :
        theorem Set.Nonempty.empty_ssubset {α : Type u} {s : Set α} :

        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.mem_univ {α : Type u} (x : α) :
        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
        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 α] :
        Set.Nonempty ss = 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, ¬a s
        theorem Set.not_subset_iff_exists_mem_not_mem {α : Type u_1} {s : Set α} {t : Set α} :
        ¬s t x, x s ¬x t
        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

        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} :
        IsAssociative (Set α) fun x x_1 => x x_1
        instance Set.union_isComm {α : Type u} :
        IsCommutative (Set α) fun x x_1 => x x_1
        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_iff_subset {α : Type u} {s : Set α} {t : Set α} :
        s t = s t s
        @[simp]
        theorem Set.union_eq_right_iff_subset {α : 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} :
        IsAssociative (Set α) fun x x_1 => x x_1
        instance Set.inter_isComm {α : Type u} :
        IsCommutative (Set α) fun x x_1 => x x_1
        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_iff_subset {α : Type u} {s : Set α} {t : Set α} :
        s t = s s t
        @[simp]
        theorem Set.inter_eq_right_iff_subset {α : Type u} {s : Set α} {t : Set α} :
        s t = 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_distrib_left {α : Type u} (s : Set α) (t : Set α) (u : Set α) :
        s (t u) = s t s u
        theorem Set.inter_union_distrib_left {α : Type u} {s : Set α} {t : Set α} {u : Set α} :
        s (t u) = s t s u
        theorem Set.inter_distrib_right {α : Type u} (s : Set α) (t : Set α) (u : Set α) :
        (s t) u = s u t 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_distrib_left {α : Type u} (s : Set α) (t : Set α) (u : Set α) :
        s t u = (s t) (s u)
        theorem Set.union_inter_distrib_left {α : Type u} {s : Set α} {t : Set α} {u : Set α} :
        s t u = (s t) (s u)
        theorem Set.union_distrib_right {α : Type u} (s : Set α) (t : Set α) (u : Set α) :
        s t u = (s u) (t u)
        theorem Set.inter_union_distrib_right {α : Type u} {s : Set α} {t : Set α} {u : Set α} :
        s t u = (s u) (t u)
        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 s¬b sb = 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 : α} :
        ¬a ss 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 ¬a s
        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
        theorem Set.insert_subset_insert_iff {α : Type u} {a : α} {s : Set α} {t : Set α} (ha : ¬a s) :
        insert a s insert a t s t
        theorem Set.subset_insert_iff_of_not_mem {α : Type u} {a : α} {s : Set α} {t : Set α} (ha : ¬a s) :
        s insert a t s t
        theorem Set.ssubset_iff_insert {α : Type u} {s : Set α} {t : Set α} :
        s t a x, insert a s t
        theorem Set.ssubset_insert {α : Type u} {s : Set α} {a : α} (h : ¬a s) :
        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 α) :
        instance Set.instNonemptyElemInsertSetInstInsertSet {α : Type u} (a : α) (s : Set α) :
        Nonempty ↑(insert a s)
        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 : ¬a s) :
        insert a s = insert b s a = b
        theorem Set.forall_of_forall_insert {α : Type u} {P : αProp} {a : α} {s : Set α} (H : (x : α) → x insert a sP x) (x : α) (h : x s) :
        P x
        theorem Set.forall_insert_of_forall {α : Type u} {P : αProp} {a : α} {s : Set α} (H : (x : α) → x sP x) (ha : P a) (x : α) (h : x insert a s) :
        P x
        theorem Set.bex_insert_iff {α : Type u} {P : αProp} {a : α} {s : Set α} :
        (x, x insert a s P x) P a x, x s P x
        theorem Set.ball_insert_iff {α : Type u} {P : αProp} {a : α} {s : Set α} :
        ((x : α) → x insert a sP x) P a ((x : α) → x sP x)

        Lemmas about singletons #

        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 : α) :
        @[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 α} :
        Set.Nonempty ({a} s) a s
        @[simp]
        theorem Set.inter_singleton_nonempty {α : Type u} {a : α} {s : Set α} :
        Set.Nonempty (s {a}) a s
        @[simp]
        theorem Set.singleton_inter_eq_empty {α : Type u} {a : α} {s : Set α} :
        {a} s = ¬a s
        @[simp]
        theorem Set.inter_singleton_eq_empty {α : Type u} {a : α} {s : Set α} :
        s {a} = ¬a s
        instance Set.uniqueSingleton {α : Type u} (a : α) :
        Unique {a}
        theorem Set.eq_singleton_iff_unique_mem {α : Type u} {a : α} {s : Set α} :
        s = {a} a s ∀ (x : α), x sx = a
        theorem Set.eq_singleton_iff_nonempty_unique_mem {α : Type u} {a : α} {s : Set α} :
        s = {a} Set.Nonempty s ∀ (x : α), x sx = a
        @[simp]
        theorem Set.default_coe_singleton {α : Type u} (x : α) :
        default = { val := x, property := (_ : x = x) }

        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

        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} ∀ (x : α), x s → (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 (x : α) → x sp x
        @[simp]
        theorem Set.sep_eq_empty_iff_mem_false {α : Type u} {s : Set α} {p : αProp} :
        {x | x s p x} = ∀ (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 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} ∀ (y : α), y sy = 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 : Set.Nonempty s) :
        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 =

        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 s¬a t
        theorem Set.disjoint_right {α : Type u} {s : Set α} {t : Set α} :
        Disjoint s t ∀ ⦃a : α⦄, a t¬a s
        theorem Set.not_disjoint_iff {α : Type u} {s : Set α} {t : Set α} :
        ¬Disjoint s t x, x s x t
        theorem Set.not_disjoint_iff_nonempty_inter {α : Type u} {s : Set α} {t : Set α} :
        theorem Set.Nonempty.not_disjoint {α : Type u} {s : Set α} {t : Set α} :

        Alias of the reverse direction of Set.not_disjoint_iff_nonempty_inter.

        theorem Set.disjoint_or_nonempty_inter {α : Type u} (s : Set α) (t : Set α) :
        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.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 ¬a s
        @[simp]
        theorem Set.disjoint_singleton_right {α : Type u} {a : α} {s : Set α} :
        Disjoint s {a} ¬a s
        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.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 | ¬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
        @[simp]
        theorem Set.mem_compl_iff {α : Type u} (s : Set α) (x : α) :
        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 α) :
        @[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 Set.Nonempty s
        theorem Set.nonempty_compl {α : Type u} {s : Set α} :
        Set.Nonempty s s Set.univ
        @[simp]
        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} ¬a s
        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 α} :

        Lemmas about set difference #

        theorem Set.diff_eq {α : Type u} (s : Set α) (t : Set α) :
        s \ t = s t
        @[simp]
        theorem Set.mem_diff {α : Type u} {s : Set α} {t : Set α} (x : α) :
        x s \ t x s ¬x t
        theorem Set.mem_diff_of_mem {α : Type u} {s : Set α} {t : Set α} {x : α} (h1 : x s) (h2 : ¬x t) :
        x s \ t
        theorem Set.not_mem_diff_of_mem {α : Type u} {s : Set α} {t : Set α} {x : α} (hx : x t) :
        ¬x s \ 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) :
        ¬x t
        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 α} :
        theorem Set.diff_subset {α : Type u} (s : Set α) (t : Set α) :
        s \ t s
        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 : ¬x s) :
        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 : ¬a t) :
        insert a s \ t = insert a (s \ t)
        theorem Set.insert_diff_self_of_not_mem {α : Type u} {a : α} {s : Set α} (h : ¬a s) :
        insert a s \ {a} = s
        @[simp]
        theorem Set.insert_diff_eq_singleton {α : Type u} {a : α} {s : Set α} (h : ¬a s) :
        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 : ¬a s) :
        s insert a t = s t
        theorem Set.insert_inter_of_not_mem {α : Type u} {a : α} {s : Set α} {t : Set α} (h : ¬a t) :
        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 : ¬a s) :
        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 α)} :
        theorem Set.union_eq_diff_union_diff_union_inter {α : Type u} (s : Set α) (t : Set α) :
        s t = s \ t t \ s s t

        Symmetric difference #

        theorem Set.mem_symmDiff {α : Type u} {a : α} {s : Set α} {t : Set α} :
        a s t a s ¬a t a t ¬a s
        theorem Set.symmDiff_def {α : Type u} (s : Set α) (t : Set α) :
        s t = s \ t t \ s
        theorem Set.symmDiff_subset_union {α : Type u} {s : Set α} {t : Set α} :
        s t s t
        @[simp]
        theorem Set.symmDiff_eq_empty {α : Type u} {s : Set α} {t : Set α} :
        s t = s = t
        @[simp]
        theorem Set.symmDiff_nonempty {α : Type u} {s : Set α} {t : Set α} :
        theorem Set.inter_symmDiff_distrib_left {α : Type u} (s : Set α) (t : Set α) (u : Set α) :
        s t u = (s t) (s u)
        theorem Set.inter_symmDiff_distrib_right {α : Type u} (s : Set α) (t : Set α) (u : Set α) :
        s t u = (s u) (t u)
        theorem Set.subset_symmDiff_union_symmDiff_left {α : Type u} {s : Set α} {t : Set α} {u : Set α} (h : Disjoint s t) :
        u s u t u
        theorem Set.subset_symmDiff_union_symmDiff_right {α : Type u} {s : Set α} {t : Set α} {u : Set α} (h : Disjoint t u) :
        s s t s 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 α} :
        @[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, 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, 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.

        Instances For
          @[simp]
          theorem Set.ite_inter_self {α : Type u} (t : Set α) (s : Set α) (s' : Set α) :
          Set.ite t s s' t = s t
          @[simp]
          theorem Set.ite_compl {α : Type u} (t : Set α) (s : Set α) (s' : Set α) :
          Set.ite t s s' = Set.ite t s' s
          @[simp]
          theorem Set.ite_inter_compl_self {α : Type u} (t : Set α) (s : Set α) (s' : Set α) :
          Set.ite t s s' t = s' t
          @[simp]
          theorem Set.ite_diff_self {α : Type u} (t : Set α) (s : Set α) (s' : Set α) :
          Set.ite t s s' \ t = s' \ t
          @[simp]
          theorem Set.ite_same {α : Type u} (t : Set α) (s : Set α) :
          Set.ite t s s = s
          @[simp]
          theorem Set.ite_left {α : Type u} (s : Set α) (t : Set α) :
          Set.ite s s t = s t
          @[simp]
          theorem Set.ite_right {α : Type u} (s : Set α) (t : Set α) :
          Set.ite s t s = t s
          @[simp]
          theorem Set.ite_empty {α : Type u} (s : Set α) (s' : Set α) :
          Set.ite s s' = s'
          @[simp]
          theorem Set.ite_univ {α : Type u} (s : Set α) (s' : Set α) :
          Set.ite Set.univ s s' = s
          @[simp]
          theorem Set.ite_empty_left {α : Type u} (t : Set α) (s : Set α) :
          Set.ite t s = s \ t
          @[simp]
          theorem Set.ite_empty_right {α : Type u} (t : Set α) (s : Set α) :
          Set.ite t 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₂') :
          Set.ite t s₁ s₁' Set.ite t s₂ s₂'
          theorem Set.ite_subset_union {α : Type u} (t : Set α) (s : Set α) (s' : Set α) :
          Set.ite t s s' s s'
          theorem Set.inter_subset_ite {α : Type u} (t : Set α) (s : Set α) (s' : Set α) :
          s s' Set.ite t s s'
          theorem Set.ite_inter_inter {α : Type u} (t : Set α) (s₁ : Set α) (s₂ : Set α) (s₁' : Set α) (s₂' : Set α) :
          Set.ite t (s₁ s₂) (s₁' s₂') = Set.ite t s₁ s₁' Set.ite t s₂ s₂'
          theorem Set.ite_inter {α : Type u} (t : Set α) (s₁ : Set α) (s₂ : Set α) (s : Set α) :
          Set.ite t (s₁ s) (s₂ s) = Set.ite t 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) :
          Set.ite t s₁ s₂ s = s₁ s
          theorem Set.subset_ite {α : Type u} {t : Set α} {s : Set α} {s' : Set α} {u : Set α} :
          u Set.ite t s s' u t s u \ t s'

          Subsingleton #

          def Set.Subsingleton {α : Type u} (s : Set α) :

          A set s is a Subsingleton if it has at most one element.

          Instances For
            theorem Set.Subsingleton.anti {α : Type u} {s : Set α} {t : Set α} (ht : Set.Subsingleton t) (hst : s t) :
            theorem Set.Subsingleton.eq_singleton_of_mem {α : Type u} {s : Set α} (hs : Set.Subsingleton s) {x : α} (hx : x s) :
            s = {x}
            @[simp]
            theorem Set.subsingleton_singleton {α : Type u} {a : α} :
            theorem Set.subsingleton_of_subset_singleton {α : Type u} {a : α} {s : Set α} (h : s {a}) :
            theorem Set.subsingleton_of_forall_eq {α : Type u} {s : Set α} (a : α) (h : ∀ (b : α), b sb = a) :
            theorem Set.subsingleton_iff_singleton {α : Type u} {s : Set α} {x : α} (hx : x s) :
            theorem Set.Subsingleton.eq_empty_or_singleton {α : Type u} {s : Set α} (hs : Set.Subsingleton s) :
            s = x, s = {x}
            theorem Set.Subsingleton.induction_on {α : Type u} {s : Set α} {p : Set αProp} (hs : Set.Subsingleton s) (he : p ) (h₁ : (x : α) → p {x}) :
            p s
            @[simp]
            theorem Set.subsingleton_coe {α : Type u} (s : Set α) :

            s, coerced to a type, is a subsingleton type if and only if s is a subsingleton set.

            The coe_sort of a set s in a subsingleton type is a subsingleton. For the corresponding result for Subtype, see subtype.subsingleton.

            Nontrivial #

            def Set.Nontrivial {α : Type u} (s : Set α) :

            A set s is Set.Nontrivial if it has at least two distinct elements.

            Instances For
              theorem Set.nontrivial_of_mem_mem_ne {α : Type u} {s : Set α} {x : α} {y : α} (hx : x s) (hy : y s) (hxy : x y) :
              noncomputable def Set.Nontrivial.choose {α : Type u} {s : Set α} (hs : Set.Nontrivial s) :
              α × α

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

              Instances For
                theorem Set.Nontrivial.mono {α : Type u} {s : Set α} {t : Set α} (hs : Set.Nontrivial s) (hst : s t) :
                theorem Set.nontrivial_pair {α : Type u} {x : α} {y : α} (hxy : x y) :
                theorem Set.nontrivial_of_pair_subset {α : Type u} {s : Set α} {x : α} {y : α} (hxy : x y) (h : {x, y} s) :
                theorem Set.Nontrivial.pair_subset {α : Type u} {s : Set α} (hs : Set.Nontrivial s) :
                x y x_1, {x, y} s
                theorem Set.nontrivial_iff_pair_subset {α : Type u} {s : Set α} :
                Set.Nontrivial s x y x_1, {x, y} s
                theorem Set.nontrivial_of_exists_ne {α : Type u} {s : Set α} {x : α} (hx : x s) (h : y, y s y x) :
                theorem Set.Nontrivial.exists_ne {α : Type u} {s : Set α} (hs : Set.Nontrivial s) (z : α) :
                x, x s x z
                theorem Set.nontrivial_iff_exists_ne {α : Type u} {s : Set α} {x : α} (hx : x s) :
                Set.Nontrivial s y, y s y x
                theorem Set.nontrivial_of_lt {α : Type u} {s : Set α} [Preorder α] {x : α} {y : α} (hx : x s) (hy : y s) (hxy : x < y) :
                theorem Set.nontrivial_of_exists_lt {α : Type u} {s : Set α} [Preorder α] (H : x x_1 y x_2, x < y) :
                theorem Set.Nontrivial.exists_lt {α : Type u} {s : Set α} [LinearOrder α] (hs : Set.Nontrivial s) :
                x x_1 y x_2, x < y
                theorem Set.nontrivial_iff_exists_lt {α : Type u} {s : Set α} [LinearOrder α] :
                Set.Nontrivial s x x_1 y x_2, x < y
                theorem Set.Nontrivial.nonempty {α : Type u} {s : Set α} (hs : Set.Nontrivial s) :
                theorem Set.Nontrivial.ne_empty {α : Type u} {s : Set α} (hs : Set.Nontrivial s) :
                @[simp]
                theorem Set.not_nontrivial_singleton {α : Type u} {x : α} :
                theorem Set.Nontrivial.ne_singleton {α : Type u} {s : Set α} {x : α} (hs : Set.Nontrivial s) :
                s {x}
                theorem Set.Nontrivial.not_subset_singleton {α : Type u} {s : Set α} {x : α} (hs : Set.Nontrivial s) :
                ¬s {x}
                @[simp]
                @[simp]
                theorem Set.nontrivial_coe_sort {α : Type u} {s : Set α} :

                s, coerced to a type, is a nontrivial type if and only if s is a nontrivial set.

                theorem Set.Nontrivial.coe_sort {α : Type u} {s : Set α} :

                Alias of the reverse direction of Set.nontrivial_coe_sort.


                s, coerced to a type, is a nontrivial type if and only if s is a nontrivial set.

                theorem Set.nontrivial_of_nontrivial_coe {α : Type u} {s : Set α} (hs : Nontrivial s) :

                A type with a set s whose coe_sort is a nontrivial type is nontrivial. For the corresponding result for Subtype, see Subtype.nontrivial_iff_exists_ne.

                theorem Set.nontrivial_mono {α : Type u_1} {s : Set α} {t : Set α} (hst : s t) (hs : Nontrivial s) :

                Alias of the reverse direction of Set.not_nontrivial_iff.

                Alias of the reverse direction of Set.not_subsingleton_iff.

                theorem Set.eq_singleton_or_nontrivial {α : Type u} {a : α} {s : Set α} (ha : a s) :
                theorem Set.nontrivial_iff_ne_singleton {α : Type u} {a : α} {s : Set α} (ha : a s) :
                theorem Set.monotoneOn_iff_monotone {α : Type u} {β : Type v} {s : Set α} [Preorder α] [Preorder β] {f : αβ} :
                MonotoneOn f s Monotone fun a => f a
                theorem Set.antitoneOn_iff_antitone {α : Type u} {β : Type v} {s : Set α} [Preorder α] [Preorder β] {f : αβ} :
                AntitoneOn f s Antitone fun a => f a
                theorem Set.strictMonoOn_iff_strictMono {α : Type u} {β : Type v} {s : Set α} [Preorder α] [Preorder β] {f : αβ} :
                StrictMonoOn f s StrictMono fun a => f a
                theorem Set.strictAntiOn_iff_strictAnti {α : Type u} {β : Type v} {s : Set α} [Preorder α] [Preorder β] {f : αβ} :
                StrictAntiOn f s StrictAnti fun a => f a

                Monotonicity on singletons #

                theorem Set.Subsingleton.monotoneOn {α : Type u} {β : Type v} {s : Set α} [Preorder α] [Preorder β] (f : αβ) (h : Set.Subsingleton s) :
                theorem Set.Subsingleton.antitoneOn {α : Type u} {β : Type v} {s : Set α} [Preorder α] [Preorder β] (f : αβ) (h : Set.Subsingleton s) :
                theorem Set.Subsingleton.strictMonoOn {α : Type u} {β : Type v} {s : Set α} [Preorder α] [Preorder β] (f : αβ) (h : Set.Subsingleton s) :
                theorem Set.Subsingleton.strictAntiOn {α : Type u} {β : Type v} {s : Set α} [Preorder α] [Preorder β] (f : αβ) (h : Set.Subsingleton s) :
                @[simp]
                theorem Set.monotoneOn_singleton {α : Type u} {β : Type v} {a : α} [Preorder α] [Preorder β] (f : αβ) :
                @[simp]
                theorem Set.antitoneOn_singleton {α : Type u} {β : Type v} {a : α} [Preorder α] [Preorder β] (f : αβ) :
                @[simp]
                theorem Set.strictMonoOn_singleton {α : Type u} {β : Type v} {a : α} [Preorder α] [Preorder β] (f : αβ) :
                @[simp]
                theorem Set.strictAntiOn_singleton {α : Type u} {β : Type v} {a : α} [Preorder α] [Preorder β] (f : αβ) :