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:

• f : α → β is a function,

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

• t : Set β is a subset of β.

Definitions in the file:

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

• Subsingleton s : Prop : the predicate saying that s has at most one element.

• Nontrivial s : Prop : the predicate saying that s has at least two distinct elements.

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

Notation

• sᶜ for the complement of s

Implementation notes

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

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

Tags

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

Set coercion to a type

instance Set.instBooleanAlgebraSet {α : Type u_1} : BooleanAlgebra (Set α)

Equations

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

instance Set.instHasSSubsetSet {α : Type u_1} : HasSSubset (Set α)

Equations

• Set.instHasSSubsetSet = { SSubset := fun x x_1 => x < x_1 }

@[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 ≤ t → s ⊆ t

Alias of the forward direction of Set.le_iff_subset.

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

Alias of the reverse direction of Set.le_iff_subset.

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

Alias of the forward direction of Set.lt_iff_ssubset.

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

Alias of the reverse direction of Set.lt_iff_ssubset.

@[reducible]

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

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

Equations

• ↑s = { x // x ∈ s }

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

Coercion from a set to the corresponding subtype.

Equations

• Set.instCoeSortSetType = { coe := Set.Elem }

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

Equations

• Set.PiSetCoe.canLift = Set.PiSetCoe.canLift.proof_1

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

Equations

• Set.PiSetCoe.canLift' = Set.PiSetCoe.canLift'.proof_1

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

Equations

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

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

@[simp]

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

theorem SetCoe.forall {α : Type u} {s : Set α} {p : ↑s → Prop} : ((x : ↑s) → p x) ↔ (x : α) → (h : x ∈ s) → p { val := x, property := h }

theorem SetCoe.exists {α : Type u} {s : Set α} {p : ↑s → Prop} : (∃ x, p x) ↔ ∃ x h, p { val := x, property := h }

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

theorem SetCoe.forall' {α : Type u} {s : Set α} {p : (x : α) → x ∈ s → Prop} : ((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 = ↑b → a = 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 = t → s ⊆ t

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

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

Equations

• Set.instInhabitedSet = { 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} : ((a : α) → a ∈ s → (b : β) → p a b) ↔ (b : β) → (a : α) → a ∈ s → p 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

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

@[simp]

theorem Set.setOf_subset_setOf {α : Type u} {p : α → Prop} {q : α → Prop} : {a | p a} ⊆ {a | q a} ↔ (a : α) → p a → q 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

Equations

• @Set.instIsReflSetSubsetInstHasSubsetSet = @Set.instIsReflSetSubsetInstHasSubsetSet.proof_1

instance Set.instIsTransSetSubsetInstHasSubsetSet {α : Type u} : IsTrans (Set α) fun x x_1 => x ⊆ x_1

Equations

• @Set.instIsTransSetSubsetInstHasSubsetSet = @Set.instIsTransSetSubsetInstHasSubsetSet.proof_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

Equations

• Set.instTransSetSubsetInstHasSubsetSet = let_fun this := inferInstance; this

instance Set.instIsAntisymmSetSubsetInstHasSubsetSet {α : Type u} : IsAntisymm (Set α) fun x x_1 => x ⊆ x_1

Equations

• @Set.instIsAntisymmSetSubsetInstHasSubsetSet = @Set.instIsAntisymmSetSubsetInstHasSubsetSet.proof_1

instance Set.instIsIrreflSetSSubsetInstHasSSubsetSet {α : Type u} : IsIrrefl (Set α) fun x x_1 => x ⊂ x_1

Equations

• @Set.instIsIrreflSetSSubsetInstHasSSubsetSet = @Set.instIsIrreflSetSSubsetInstHasSSubsetSet.proof_1

instance Set.instIsTransSetSSubsetInstHasSSubsetSet {α : Type u} : IsTrans (Set α) fun x x_1 => x ⊂ x_1

Equations

• @Set.instIsTransSetSSubsetInstHasSSubsetSet = @Set.instIsTransSetSSubsetInstHasSSubsetSet.proof_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

Equations

• Set.instTransSetSSubsetInstHasSSubsetSet = let_fun this := inferInstance; this

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

Equations

• Set.instTransSetSSubsetInstHasSSubsetSetSubsetInstHasSubsetSet = let_fun this := inferInstance; this

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

Equations

• Set.instTransSetSubsetInstHasSubsetSetSSubsetInstHasSSubsetSet = let_fun this := inferInstance; this

instance Set.instIsAsymmSetSSubsetInstHasSSubsetSet {α : Type u} : IsAsymm (Set α) fun x x_1 => x ⊂ x_1

Equations

• @Set.instIsAsymmSetSSubsetInstHasSSubsetSet = @Set.instIsAsymmSetSSubsetInstHasSSubsetSet.proof_1

instance Set.instIsNonstrictStrictOrderSetSubsetInstHasSubsetSetSSubsetInstHasSSubsetSet {α : Type u} : IsNonstrictStrictOrder (Set α) (fun x x_1 => x ⊆ x_1) fun x x_1 => x ⊂ x_1

Equations

• @Set.instIsNonstrictStrictOrderSetSubsetInstHasSubsetSetSSubsetInstHasSSubsetSet = @Set.instIsNonstrictStrictOrderSetSubsetInstHasSubsetSetSSubsetInstHasSSubsetSet.proof_1

theorem Set.subset_def {α : Type u} {s : Set α} {t : Set α} : (s ⊆ t) = ∀ (x : α), x ∈ s → 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 ⊆ b → b ⊆ a → a = 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 : α) : ¬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 α) : Prop

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.

Equations

• Set.Nonempty s = ∃ x, x ∈ s

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

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

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) : Set.Nonempty s

theorem Set.Nonempty.not_subset_empty {α : Type u} {s : Set α} : Set.Nonempty s → ¬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.

Equations

• Set.Nonempty.some h = Classical.choose h

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

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

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

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

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

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

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

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

@[simp]

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

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

theorem Set.Nonempty.right {α : Type u} {s : Set α} {t : Set α} (h : Set.Nonempty (s ∩ t)) : Set.Nonempty 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

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

@[simp]

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

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

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

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

Equations

• @Set.univ.nonempty = @Set.univ.nonempty.proof_1

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

Lemmas about the empty set

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

Equations

• Set.uniqueEmpty = { toInhabited := { default := ∅ }, uniq := (_ : ∀ (s : Set α), s = ∅) }

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

See also Set.nonempty_iff_ne_empty.

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

See also Set.not_nonempty_iff_eq_empty.

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

See also nonempty_iff_ne_empty'.

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

See also not_nonempty_iff_eq_empty'.

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

Alias of the forward direction of Set.nonempty_iff_ne_empty.

---

See also Set.not_nonempty_iff_eq_empty.

@[simp]

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

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

theorem Set.eq_empty_or_nonempty {α : Type u} (s : Set α) : s = ∅ ∨ Set.Nonempty 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

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

Equations

• Set.instIsEmptyElemEmptyCollectionSetInstEmptyCollectionSet = Set.instIsEmptyElemEmptyCollectionSetInstEmptyCollectionSet.proof_1

@[simp]

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

theorem Set.Nonempty.empty_ssubset {α : Type u} {s : Set α} : Set.Nonempty s → ∅ ⊂ 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.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 ⊆ s → s = 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 s → s = 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

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

Equations

• @Set.nontrivial_of_nonempty = @Set.nontrivial_of_nonempty.proof_1

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 ∈ a → x ∈ a ∪ b

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

theorem Set.mem_or_mem_of_mem_union {α : Type u} {x : α} {a : 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 ∈ a → P) (H₃ : x ∈ b → P) : 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

Equations

• @Set.union_isAssoc = @Set.union_isAssoc.proof_1

instance Set.union_isComm {α : Type u} : IsCommutative (Set α) fun x x_1 => x ∪ x_1

Equations

• @Set.union_isComm = @Set.union_isComm.proof_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 {α : 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 α) : a ∩ ∅ = ∅

@[simp]

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

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

Equations

• @Set.inter_isAssoc = @Set.inter_isAssoc.proof_1

instance Set.inter_isComm {α : Type u} : IsCommutative (Set α) fun x x_1 => x ∩ x_1

Equations

• @Set.inter_isComm = @Set.inter_isComm.proof_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 {α : 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

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

theorem Set.inter_eq_self_of_subset_right {α : Type u} {s : Set α} {t : Set α} : t ⊆ s → s ∩ 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 ∈ s → x ∈ insert y s

theorem Set.eq_or_mem_of_mem_insert {α : Type u} {x : α} {a : α} {s : Set α} : x ∈ insert a s → x = a ∨ x ∈ s

theorem Set.mem_of_mem_insert_of_ne {α : Type u} {a : α} {b : α} {s : Set α} : b ∈ insert a s → b ≠ a → b ∈ s

theorem Set.eq_of_not_mem_of_mem_insert {α : Type u} {a : α} {b : α} {s : Set α} : b ∈ insert a s → ¬b ∈ s → b = 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 ∈ s → s ≠ 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 α) : Set.Nonempty (insert a s)

instance Set.instNonemptyElemInsertSetInstInsertSet {α : Type u} (a : α) (s : Set α) : Nonempty ↑(insert a s)

Equations

• @Set.instNonemptyElemInsertSetInstInsertSet = @Set.instNonemptyElemInsertSetInstInsertSet.proof_1

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 s → P x) (x : α) (h : x ∈ s) : P x

theorem Set.forall_insert_of_forall {α : Type u} {P : α → Prop} {a : α} {s : Set α} (H : (x : α) → x ∈ s → P 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 s → P x) ↔ P a ∧ ((x : α) → x ∈ s → P x)

Lemmas about singletons

instance Set.instIsLawfulSingletonSetInstEmptyCollectionSetInstInsertSetInstSingletonSet {α : Type u} : IsLawfulSingleton α (Set α)

Equations

• @Set.instIsLawfulSingletonSetInstEmptyCollectionSetInstInsertSetInstSingletonSet = @Set.instIsLawfulSingletonSetInstEmptyCollectionSetInstInsertSetInstSingletonSet.proof_1

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.singleton_injective {α : Type u} : Function.Injective singleton

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 : α) : Set.Nonempty {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

theorem Set.nmem_singleton_empty {α : Type u} {s : Set α} : ¬s ∈ {∅} ↔ Set.Nonempty s

instance Set.uniqueSingleton {α : Type u} (a : α) : Unique ↑{a}

Equations

• Set.uniqueSingleton a = { toInhabited := { default := { val := a, property := (_ : a ∈ {a}) } }, uniq := (_ : ∀ (x : ↑{a}), x = default) }

theorem Set.eq_singleton_iff_unique_mem {α : Type u} {a : α} {s : Set α} : s = {a} ↔ a ∈ s ∧ ∀ (x : α), x ∈ s → x = a

theorem Set.eq_singleton_iff_nonempty_unique_mem {α : Type u} {a : α} {s : Set α} : s = {a} ↔ Set.Nonempty s ∧ ∀ (x : α), x ∈ s → x = 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 ∈ s → p 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 ∈ s → 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 : 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 α} : Disjoint s t ↔ s ∩ t ⊆ ∅

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 t → s ∩ 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 α} : ¬Disjoint s t ↔ Set.Nonempty (s ∩ t)

theorem Set.Nonempty.not_disjoint {α : Type u} {s : Set α} {t : Set α} : Set.Nonempty (s ∩ t) → ¬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 ∨ Set.Nonempty (s ∩ t)

theorem Set.disjoint_iff_forall_ne {α : Type u} {s : Set α} {t : Set α} : Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ t → a ≠ b

theorem Disjoint.ne_of_mem {α : Type u} {s : Set α} {t : Set α} : Disjoint s t → ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ t → a ≠ 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) : Disjoint s t

theorem Set.disjoint_of_subset_right {α : Type u} {s : Set α} {t : Set α} {u : Set α} (h : t ⊆ u) (d : Disjoint s u) : Disjoint s t

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 α} : Disjoint (s ∪ t) u ↔ Disjoint s u ∧ Disjoint t u

@[simp]

theorem Set.disjoint_union_right {α : Type u} {s : Set α} {t : Set α} {u : Set α} : Disjoint s (t ∪ u) ↔ Disjoint s t ∧ Disjoint s u

@[simp]

theorem Set.disjoint_empty {α : Type u} (s : Set α) : Disjoint s ∅

@[simp]

theorem Set.empty_disjoint {α : Type u} (s : Set α) : Disjoint ∅ s

@[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 α) : s ∩ sᶜ = ∅

@[simp]

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

@[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.nonempty_compl_of_nontrivial {α : Type u} [Nontrivial α] (x : α) : Set.Nonempty {x}ᶜ

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) : sᶜ ⊆ tᶜ

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

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

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

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

theorem Disjoint.subset_compl_right {α : Type u} {s : Set α} {t : Set α} : Disjoint s t → s ⊆ 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 s → s ⊆ 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 ⊆ s → Disjoint 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 ⊆ t → Disjoint 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 α} : Set.Nonempty (s ∩ tᶜ) ↔ ¬s ⊆ t

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 α} : Set.Nonempty (s \ t) ↔ ¬s ⊆ t

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 α) : ∅ \ s = ∅

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 α)} : s ∈ t \ {∅} ↔ s ∈ t ∧ Set.Nonempty s

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 α} : Set.Nonempty (s ∆ t) ↔ s ≠ t

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 α} : Set.Nonempty (𝒫 s)

@[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 : p → Set α) (t : ¬p → Set α) (x : α) : (x ∈ if h : p then s h else t h) ↔ (∀ (h : p), x ∈ s h) ∧ ∀ (h : ¬p), x ∈ t h

theorem Set.mem_dite_univ_right {α : Type u} (p : Prop) [Decidable p] (t : p → Set α) (x : α) : (x ∈ if h : p then t h else 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) ↔ p → x ∈ t

theorem Set.mem_dite_univ_left {α : Type u} (p : Prop) [Decidable p] (t : ¬p → Set α) (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) ↔ ¬p → x ∈ t

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

@[simp]

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

theorem Set.mem_dite_empty_left {α : Type u} (p : Prop) [Decidable p] (t : ¬p → Set α) (x : α) : (x ∈ if h : p then ∅ else t h) ↔ ∃ h, 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

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

@[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 α) : Prop

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

Equations

• Set.Subsingleton s = ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y

theorem Set.Subsingleton.anti {α : Type u} {s : Set α} {t : Set α} (ht : Set.Subsingleton t) (hst : s ⊆ t) : Set.Subsingleton s

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_empty {α : Type u} : Set.Subsingleton ∅

@[simp]

theorem Set.subsingleton_singleton {α : Type u} {a : α} : Set.Subsingleton {a}

theorem Set.subsingleton_of_subset_singleton {α : Type u} {a : α} {s : Set α} (h : s ⊆ {a}) : Set.Subsingleton s

theorem Set.subsingleton_of_forall_eq {α : Type u} {s : Set α} (a : α) (h : ∀ (b : α), b ∈ s → b = a) : Set.Subsingleton s

theorem Set.subsingleton_iff_singleton {α : Type u} {s : Set α} {x : α} (hx : x ∈ s) : Set.Subsingleton s ↔ s = {x}

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

theorem Set.subsingleton_univ {α : Type u} [Subsingleton α] : Set.Subsingleton Set.univ

theorem Set.subsingleton_of_univ_subsingleton {α : Type u} (h : Set.Subsingleton Set.univ) : Subsingleton α

@[simp]

theorem Set.subsingleton_univ_iff {α : Type u} : Set.Subsingleton Set.univ ↔ Subsingleton α

theorem Set.subsingleton_of_subsingleton {α : Type u} [Subsingleton α] {s : Set α} : Set.Subsingleton s

theorem Set.subsingleton_isTop (α : Type u_1) [PartialOrder α] : Set.Subsingleton {x | IsTop x}

theorem Set.subsingleton_isBot (α : Type u_1) [PartialOrder α] : Set.Subsingleton {x | IsBot x}

theorem Set.exists_eq_singleton_iff_nonempty_subsingleton {α : Type u} {s : Set α} : (∃ a, s = {a}) ↔ Set.Nonempty s ∧ Set.Subsingleton s

@[simp]

theorem Set.subsingleton_coe {α : Type u} (s : Set α) : Subsingleton ↑s ↔ Set.Subsingleton s

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

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

instance Set.subsingleton_coe_of_subsingleton {α : Type u} [Subsingleton α] {s : Set α} : Subsingleton ↑s

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

Equations

• @Set.subsingleton_coe_of_subsingleton = @Set.subsingleton_coe_of_subsingleton.proof_1

Nontrivial

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

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

Equations

• Set.Nontrivial s = ∃ x, x ∈ s ∧ ∃ y, y ∈ s ∧ x ≠ y

theorem Set.nontrivial_of_mem_mem_ne {α : Type u} {s : Set α} {x : α} {y : α} (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y) : Set.Nontrivial s

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.

Equations

• Set.Nontrivial.choose hs = (Exists.choose hs, Exists.choose (_ : ∃ y, y ∈ s ∧ Exists.choose hs ≠ y))

theorem Set.Nontrivial.choose_fst_mem {α : Type u} {s : Set α} (hs : Set.Nontrivial s) : (Set.Nontrivial.choose hs).fst ∈ s

theorem Set.Nontrivial.choose_snd_mem {α : Type u} {s : Set α} (hs : Set.Nontrivial s) : (Set.Nontrivial.choose hs).snd ∈ s

theorem Set.Nontrivial.choose_fst_ne_choose_snd {α : Type u} {s : Set α} (hs : Set.Nontrivial s) : (Set.Nontrivial.choose hs).fst ≠ (Set.Nontrivial.choose hs).snd

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

theorem Set.nontrivial_pair {α : Type u} {x : α} {y : α} (hxy : x ≠ y) : Set.Nontrivial {x, y}

theorem Set.nontrivial_of_pair_subset {α : Type u} {s : Set α} {x : α} {y : α} (hxy : x ≠ y) (h : {x, y} ⊆ s) : Set.Nontrivial 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) : Set.Nontrivial s

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) : Set.Nontrivial s

theorem Set.nontrivial_of_exists_lt {α : Type u} {s : Set α} [Preorder α] (H : ∃ x x_1 y x_2, x < y) : Set.Nontrivial s

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) : Set.Nonempty s

theorem Set.Nontrivial.ne_empty {α : Type u} {s : Set α} (hs : Set.Nontrivial s) : s ≠ ∅

theorem Set.Nontrivial.not_subset_empty {α : Type u} {s : Set α} (hs : Set.Nontrivial s) : ¬s ⊆ ∅

@[simp]

theorem Set.not_nontrivial_empty {α : Type u} : ¬Set.Nontrivial ∅

@[simp]

theorem Set.not_nontrivial_singleton {α : Type u} {x : α} : ¬Set.Nontrivial {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}

theorem Set.nontrivial_univ {α : Type u} [Nontrivial α] : Set.Nontrivial Set.univ

theorem Set.nontrivial_of_univ_nontrivial {α : Type u} (h : Set.Nontrivial Set.univ) : Nontrivial α

@[simp]

theorem Set.nontrivial_univ_iff {α : Type u} : Set.Nontrivial Set.univ ↔ Nontrivial α

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

@[simp]

theorem Set.nontrivial_coe_sort {α : Type u} {s : Set α} : Nontrivial ↑s ↔ Set.Nontrivial s

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 α} : Set.Nontrivial s → Nontrivial ↑s

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) : Nontrivial α

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) : Nontrivial ↑t

@[simp]

theorem Set.not_subsingleton_iff {α : Type u} {s : Set α} : ¬Set.Subsingleton s ↔ Set.Nontrivial s

@[simp]

theorem Set.not_nontrivial_iff {α : Type u} {s : Set α} : ¬Set.Nontrivial s ↔ Set.Subsingleton s

theorem Set.Subsingleton.not_nontrivial {α : Type u} {s : Set α} : Set.Subsingleton s → ¬Set.Nontrivial s

Alias of the reverse direction of Set.not_nontrivial_iff.

theorem Set.Nontrivial.not_subsingleton {α : Type u} {s : Set α} : Set.Nontrivial s → ¬Set.Subsingleton s

Alias of the reverse direction of Set.not_subsingleton_iff.

theorem Set.subsingleton_or_nontrivial {α : Type u} (s : Set α) : Set.Subsingleton s ∨ Set.Nontrivial s

theorem Set.eq_singleton_or_nontrivial {α : Type u} {a : α} {s : Set α} (ha : a ∈ s) : s = {a} ∨ Set.Nontrivial s

theorem Set.nontrivial_iff_ne_singleton {α : Type u} {a : α} {s : Set α} (ha : a ∈ s) : Set.Nontrivial s ↔ s ≠ {a}

theorem Set.Nonempty.exists_eq_singleton_or_nontrivial {α : Type u} {s : Set α} : Set.Nonempty s → (∃ a, s = {a}) ∨ Set.Nontrivial s

theorem Set.univ_eq_true_false : Set.univ = {True, False}

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) : MonotoneOn f s

theorem Set.Subsingleton.antitoneOn {α : Type u} {β : Type v} {s : Set α} [Preorder α] [Preorder β] (f : α → β) (h : Set.Subsingleton s) : AntitoneOn f s

theorem Set.Subsingleton.strictMonoOn {α : Type u} {β : Type v} {s : Set α} [Preorder α] [Preorder β] (f : α → β) (h : Set.Subsingleton s) : StrictMonoOn f s

theorem Set.Subsingleton.strictAntiOn {α : Type u} {β : Type v} {s : Set α} [Preorder α] [Preorder β] (f : α → β) (h : Set.Subsingleton s) : StrictAntiOn f s

@[simp]

theorem Set.monotoneOn_singleton {α : Type u} {β : Type v} {a : α} [Preorder α] [Preorder β] (f : α → β) : MonotoneOn f {a}

@[simp]

theorem Set.antitoneOn_singleton {α : Type u} {β : Type v} {a : α} [Preorder α] [Preorder β] (f : α → β) : AntitoneOn f {a}

@[simp]

theorem Set.strictMonoOn_singleton {α : Type u} {β : Type v} {a : α} [Preorder α] [Preorder β] (f : α → β) : StrictMonoOn f {a}

@[simp]

theorem Set.strictAntiOn_singleton {α : Type u} {β : Type v} {a : α} [Preorder α] [Preorder β] (f : α → β) : StrictAntiOn 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 ↔ ∃ a x b x c x, 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 ↔ ∃ a x b x c x, 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 α} : Set.Nonempty (f s) ↔ Set.Nonempty s

Lemmas about inclusion, the injection of subtypes induced by ⊆

def Set.inclusion {α : Type u_1} {s : Set α} {t : Set α} (h : s ⊆ t) : ↑s → ↑t

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

Equations

• Set.inclusion h x = { val := ↑x, property := (_ : ↑x ∈ t) }

@[simp]

theorem Set.inclusion_self {α : Type u_1} {s : Set α} (x : ↑s) : Set.inclusion (_ : s ⊆ s) x = x

theorem Set.inclusion_eq_id {α : Type u_1} {s : Set α} (h : s ⊆ s) : Set.inclusion h = id

@[simp]

theorem Set.inclusion_mk {α : Type u_1} {s : Set α} {t : Set α} {h : s ⊆ t} (a : α) (ha : a ∈ s) : Set.inclusion h { val := a, property := ha } = { val := a, property := h a ha }

theorem Set.inclusion_right {α : Type u_1} {s : Set α} {t : Set α} (h : s ⊆ t) (x : ↑t) (m : ↑x ∈ s) : Set.inclusion h { val := ↑x, property := m } = x

@[simp]

theorem Set.inclusion_inclusion {α : Type u_1} {s : Set α} {t : Set α} {u : Set α} (hst : s ⊆ t) (htu : t ⊆ u) (x : ↑s) : Set.inclusion htu (Set.inclusion hst x) = Set.inclusion (_ : s ⊆ u) x

@[simp]

theorem Set.inclusion_comp_inclusion {α : Type u_2} {s : Set α} {t : Set α} {u : Set α} (hst : s ⊆ t) (htu : t ⊆ u) : Set.inclusion htu ∘ Set.inclusion hst = Set.inclusion (_ : s ⊆ 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.inclusion_injective {α : Type u_1} {s : Set α} {t : Set α} (h : s ⊆ t) : Function.Injective (Set.inclusion h)

@[simp]

theorem Set.inclusion_inj {α : Type u_1} {s : Set α} {t : Set α} (h : s ⊆ t) {x : ↑s} {y : ↑s} : Set.inclusion h x = Set.inclusion h y ↔ x = y

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} : Set.inclusion h x ≤ Set.inclusion h y ↔ x ≤ y

@[simp]

theorem Set.inclusion_lt_inclusion {α : Type u_1} [Preorder α] {s : Set α} {t : Set α} (h : s ⊆ t) {x : ↑s} {y : ↑s} : Set.inclusion h x < Set.inclusion h y ↔ x < y

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

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

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

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

• Set.decidableSdiff s t a = inferInstance

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

Equations

• Set.decidableInter s t a = inferInstance

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

Equations

• Set.decidableUnion s t a = inferInstance

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

Equations

• Set.decidableCompl s a = inferInstance

instance Set.decidableEmptyset {α : Type u} : DecidablePred fun x => x ∈ ∅

Equations

• Set.decidableEmptyset x = isFalse (_ : ¬x ∈ ∅)

instance Set.decidableUniv {α : Type u} : DecidablePred fun x => x ∈ Set.univ

Equations

• Set.decidableUniv x = isTrue (_ : x ∈ Set.univ)

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

Equations

• Set.decidableSetOf a p = inst

instance Set.decidableMemSingleton {α : Type u} {a : α} {b : α} [DecidableEq α] : Decidable (a ∈ {b})

Equations

• Set.decidableMemSingleton = Set.decidableSetOf a fun x => x = b

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 => (x : α) → x ∈ s → 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}