Mathlib.Data.Set.Basic

Set.instBooleanAlgebra instance

: BooleanAlgebra (Set α)

Full source

instance instBooleanAlgebra : BooleanAlgebra (Set α) :=
  { (inferInstance : BooleanAlgebra (α → Prop)) with
    sup := (· ∪ ·),
    le := (· ≤ ·),
    lt := fun s t => s ⊆ ts ⊆ t ∧ ¬t ⊆ s,
    inf := (· ∩ ·),
    bot := ∅,
    compl := (·ᶜ),
    top := univ,
    sdiff := (· \ ·) }

Boolean Algebra Structure on Sets

Informal description

For any type $\alpha$, the collection of sets over $\alpha$ forms a Boolean algebra with the operations of union $\cup$, intersection $\cap$, complement $(\cdot)^c$, and the relations $\subseteq$ and $=$, where the universal set is $\alpha$ itself and the empty set is the bottom element.

Set.instHasSSubset instance

: HasSSubset (Set α)

Full source

instance : HasSSubset (Set α) :=
  ⟨(· < ·)⟩

Strict Subset Relation on Sets

Informal description

For any type $\alpha$, the collection of sets over $\alpha$ is equipped with a strict subset relation $\subset$.

Set.top_eq_univ theorem

: (⊤ : Set α) = univ

Full source

@[simp]
theorem top_eq_univ : (⊤ : Set α) = univ :=
  rfl

Top Element Equals Universal Set in Boolean Algebra of Sets

Informal description

The top element in the Boolean algebra of sets over a type $\alpha$ is equal to the universal set $\text{univ}$, i.e., $\top = \text{univ}$.

Set.bot_eq_empty theorem

: (⊥ : Set α) = ∅

Full source

@[simp]
theorem bot_eq_empty : (⊥ : Set α) = ∅ :=
  rfl

Bottom Element Equals Empty Set in Boolean Algebra of Sets

Informal description

The bottom element in the Boolean algebra of sets over a type $\alpha$ is equal to the empty set, i.e., $\bot = \emptyset$.

Set.sup_eq_union theorem

: ((· ⊔ ·) : Set α → Set α → Set α) = (· ∪ ·)

Full source

@[simp]
theorem sup_eq_union : ((· ⊔ ·) : Set α → Set α → Set α) = (· ∪ ·) :=
  rfl

Supremum of Sets Equals Union

Informal description

For any type $\alpha$, the supremum operation $\sqcup$ on sets over $\alpha$ coincides with the union operation $\cup$.

Set.inf_eq_inter theorem

: ((· ⊓ ·) : Set α → Set α → Set α) = (· ∩ ·)

Full source

@[simp]
theorem inf_eq_inter : ((· ⊓ ·) : Set α → Set α → Set α) = (· ∩ ·) :=
  rfl

Infimum of Sets Equals Intersection

Informal description

For any type $\alpha$, the infimum operation $\sqcap$ on sets over $\alpha$ coincides with the set intersection operation $\cap$. That is, for any two sets $s, t : \text{Set } \alpha$, we have $s \sqcap t = s \cap t$.

Set.le_eq_subset theorem

: ((· ≤ ·) : Set α → Set α → Prop) = (· ⊆ ·)

Full source

@[simp]
theorem le_eq_subset : ((· ≤ ·) : Set α → Set α → Prop) = (· ⊆ ·) :=
  rfl

Partial Order on Sets is Subset Inclusion

Informal description

For any type $\alpha$, the partial order relation $\leq$ on sets over $\alpha$ coincides with the subset relation $\subseteq$.

Set.lt_eq_ssubset theorem

: ((· < ·) : Set α → Set α → Prop) = (· ⊂ ·)

Full source

@[simp]
theorem lt_eq_ssubset : ((· < ·) : Set α → Set α → Prop) = (· ⊂ ·) :=
  rfl

Strict Order on Sets is Strict Subset Inclusion

Informal description

For any type $\alpha$, the strict order relation $<$ on sets over $\alpha$ coincides with the strict subset relation $\subset$.

Set.le_iff_subset theorem

: s ≤ t ↔ s ⊆ t

Full source

theorem le_iff_subset : s ≤ t ↔ s ⊆ t :=
  Iff.rfl

Subset Relation Equivalent to Partial Order on Sets

Informal description

For any two sets $s$ and $t$ of type $\alpha$, the inequality $s \leq t$ holds if and only if $s$ is a subset of $t$, i.e., $s \subseteq t$.

Set.lt_iff_ssubset theorem

: s < t ↔ s ⊂ t

Full source

theorem lt_iff_ssubset : s < t ↔ s ⊂ t :=
  Iff.rfl

Strict Inequality Equivalent to Strict Subset Relation on Sets

Informal description

For any two sets $s$ and $t$ of type $\alpha$, the strict inequality $s < t$ holds if and only if $s$ is a strict subset of $t$, i.e., $s \subset t$.

Set.PiSetCoe.canLift instance

 (ι : Type u) (α : ι → Type v) [∀ i, Nonempty (α i)] (s : Set ι) :
  CanLift (∀ i : s, α i) (∀ i, α i) (fun f i => f i) fun _ => True

Full source

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

Lifting Functions from Subset to Full Index Set

Informal description

For any type family $\alpha$ indexed by $\iota$ where each $\alpha_i$ is nonempty, and any subset $s$ of $\iota$, there is a canonical way to lift functions from the subtype $\{i \in \iota \mid i \in s\}$ to $\alpha$ to functions from all of $\iota$ to $\alpha$ via the inclusion map.

Set.PiSetCoe.canLift' instance

(ι : Type u) (α : Type v) [Nonempty α] (s : Set ι) : CanLift (s → α) (ι → α) (fun f i => f i) fun _ => True

Full source

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

Lifting Functions from Subset to Full Domain for Nonempty Types

Informal description

For any type $\alpha$ that is nonempty and any subset $s$ of a type $\iota$, there exists a canonical way to lift functions from $s \to \alpha$ to $\iota \to \alpha$ via the inclusion map. Specifically, any function $f : s \to \alpha$ can be extended to a function $\tilde{f} : \iota \to \alpha$ such that $\tilde{f}(i) = f(i)$ for all $i \in s$.

instCoeTCElem instance

(s : Set α) : CoeTC s α

Full source

instance (s : Set α) : CoeTC s α := ⟨fun x => x.1⟩

Canonical Coercion from Set Subtype to Base Type

Informal description

For any set $s$ of elements of type $\alpha$, there is a canonical coercion from the type associated with $s$ to $\alpha$ itself. This means any element of the subtype corresponding to $s$ can be treated as an element of $\alpha$.

Set.coe_eq_subtype theorem

(s : Set α) : ↥s = { x // x ∈ s }

Full source

theorem Set.coe_eq_subtype (s : Set α) : ↥s = { x // x ∈ s } :=
  rfl

Coercion of Set to Subtype Equality

Informal description

For any set $s$ of elements of type $\alpha$, the coercion of $s$ to a type is equal to the subtype $\{x \mid x \in s\}$ of $\alpha$.

Set.coe_setOf theorem

(p : α → Prop) : ↥{x | p x} = { x // p x }

Full source

@[simp]
theorem Set.coe_setOf (p : α → Prop) : ↥{ x | p x } = { x // p x } :=
  rfl

Coercion of Set Comprehension to Subtype

Informal description

For any predicate $p : \alpha \to \text{Prop}$, the coercion of the set $\{x \mid p x\}$ to a type is equal to the subtype $\{x \mid p x\}$ of $\alpha$.

SetCoe.forall theorem

{s : Set α} {p : s → Prop} : (∀ x : s, p x) ↔ ∀ (x) (h : x ∈ s), p ⟨x, h⟩

Full source

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

Universal Quantification over Set Elements via Subtype

Informal description

For any set $s$ of elements of type $\alpha$ and any predicate $p$ on elements of $s$, the following are equivalent: 1. For every element $x$ in the subtype corresponding to $s$, $p(x)$ holds. 2. For every element $x$ of type $\alpha$ with $x \in s$, $p(\langle x, h\rangle)$ holds (where $h$ is the proof that $x \in s$).

SetCoe.exists theorem

{s : Set α} {p : s → Prop} : (∃ x : s, p x) ↔ ∃ (x : _) (h : x ∈ s), p ⟨x, h⟩

Full source

theorem SetCoe.exists {s : Set α} {p : s → Prop} :
    (∃ x : s, p x) ↔ ∃ (x : _) (h : x ∈ s), p ⟨x, h⟩ :=
  Subtype.exists

Existence in Subset vs Existence in Type

Informal description

For any set $s$ in type $\alpha$ and any predicate $p$ on elements of $s$, there exists an element $x$ in $s$ satisfying $p(x)$ if and only if there exists an element $x$ of type $\alpha$ with $x \in s$ such that $p(\langle x, h\rangle)$ holds (where $h$ is the proof that $x \in s$).

SetCoe.exists' theorem

{s : Set α} {p : ∀ x, x ∈ s → Prop} : (∃ (x : _) (h : x ∈ s), p x h) ↔ ∃ x : s, p x.1 x.2

Full source

theorem SetCoe.exists' {s : Set α} {p : ∀ x, x ∈ s → Prop} :
    (∃ (x : _) (h : x ∈ s), p x h) ↔ ∃ x : s, p x.1 x.2 :=
  (@SetCoe.exists _ _ fun x => p x.1 x.2).symm

Existence in Set Subtype vs Existence with Membership Proof

Informal description

For any set $s$ of elements of type $\alpha$ and any predicate $p$ on elements of $s$ with their membership proofs, the following are equivalent: 1. There exists an element $x$ of type $\alpha$ and a proof $h$ that $x \in s$ such that $p(x, h)$ holds. 2. There exists an element $x$ in the subtype corresponding to $s$ such that $p(x.1, x.2)$ holds (where $x.1$ is the underlying element and $x.2$ is the proof that $x.1 \in s$).

SetCoe.forall' theorem

{s : Set α} {p : ∀ x, x ∈ s → Prop} : (∀ (x) (h : x ∈ s), p x h) ↔ ∀ x : s, p x.1 x.2

Full source

theorem SetCoe.forall' {s : Set α} {p : ∀ x, x ∈ s → Prop} :
    (∀ (x) (h : x ∈ s), p x h) ↔ ∀ x : s, p x.1 x.2 :=
  (@SetCoe.forall _ _ fun x => p x.1 x.2).symm

Universal Quantification over Set Elements via Subtype and Membership Proof

Informal description

For any set $s$ of elements of type $\alpha$ and any predicate $p$ on elements of $s$ with their membership proofs, the following are equivalent: 1. For every element $x$ of type $\alpha$ and every proof $h$ that $x \in s$, the predicate $p(x, h)$ holds. 2. For every element $x$ in the subtype corresponding to $s$, the predicate $p(x.1, x.2)$ holds (where $x.1$ is the underlying element and $x.2$ is the proof that $x.1 \in s$).

set_coe_cast theorem

: ∀ {s t : Set α} (H' : s = t) (H : ↥s = ↥t) (x : s), cast H x = ⟨x.1, H' ▸ x.2⟩

Full source

@[simp]
theorem set_coe_cast :
    ∀ {s t : Set α} (H' : s = t) (H : ↥s = ↥t) (x : s), cast H x = ⟨x.1, H' ▸ x.2⟩
  | _, _, rfl, _, _ => rfl

Cast Equality for Set Subtypes

Informal description

For any sets $s$ and $t$ of elements of type $\alpha$, if $s = t$ and the corresponding subtypes $\uparrow s$ and $\uparrow t$ are equal (i.e., $\uparrow s = \uparrow t$), then for any element $x$ of the subtype $\uparrow s$, the cast of $x$ to $\uparrow t$ along $H$ is equal to the pair $\langle x.1, H' \triangleright x.2 \rangle$, where $x.1$ is the underlying element of $\alpha$ and $x.2$ is the proof that $x.1 \in s$.

SetCoe.ext theorem

{s : Set α} {a b : s} : (a : α) = b → a = b

Full source

theorem SetCoe.ext {s : Set α} {a b : s} : (a : α) = b → a = b :=
  Subtype.eq

Subtype Equality from Underlying Equality

Informal description

For any set $s$ of elements of type $\alpha$ and any two elements $a, b$ of the subtype corresponding to $s$, if the underlying elements $(a : \alpha)$ and $(b : \alpha)$ are equal, then $a$ and $b$ are equal as elements of the subtype.

SetCoe.ext_iff theorem

{s : Set α} {a b : s} : (↑a : α) = ↑b ↔ a = b

Full source

theorem SetCoe.ext_iff {s : Set α} {a b : s} : (↑a : α) = ↑b ↔ a = b :=
  Iff.intro SetCoe.ext fun h => h ▸ rfl

Subtype Equality Equivalence: $(a : \alpha) = (b : \alpha) \leftrightarrow a = b$ for $a, b \in s$

Informal description

For any set $s$ of elements of type $\alpha$ and any two elements $a, b$ of the subtype corresponding to $s$, the underlying elements $(a : \alpha)$ and $(b : \alpha)$ are equal if and only if $a$ and $b$ are equal as elements of the subtype.

Subtype.mem theorem

{α : Type*} {s : Set α} (p : s) : (p : α) ∈ s

Full source

/-- See also `Subtype.prop` -/
theorem Subtype.mem {α : Type*} {s : Set α} (p : s) : (p : α) ∈ s :=
  p.prop

Subtype Element Membership in Underlying Set

Informal description

For any type $\alpha$ and any subset $s \subseteq \alpha$, if $p$ is an element of the subtype corresponding to $s$, then the underlying element $(p : \alpha)$ belongs to $s$.

Eq.subset theorem

{α} {s t : Set α} : s = t → s ⊆ t

Full source

/-- Duplicate of `Eq.subset'`, which currently has elaboration problems. -/
theorem Eq.subset {α} {s t : Set α} : s = t → s ⊆ t :=
  fun h₁ _ h₂ => by rw [← h₁]; exact h₂

Equality Implies Subset Relation

Informal description

For any type $\alpha$ and any two sets $s, t \subseteq \alpha$, if $s = t$, then $s$ is a subset of $t$, i.e., $s \subseteq t$.

Set.instInhabited instance

: Inhabited (Set α)

Full source

instance : Inhabited (Set α) :=
  ⟨∅⟩

Inhabitedness of Sets Over a Type

Informal description

For any type $\alpha$, the collection of sets over $\alpha$ is inhabited (i.e., there exists at least one set of type $\alpha$).

Set.mem_of_mem_of_subset theorem

{x : α} {s t : Set α} (hx : x ∈ s) (h : s ⊆ t) : x ∈ t

Full source

@[trans]
theorem mem_of_mem_of_subset {x : α} {s t : Set α} (hx : x ∈ s) (h : s ⊆ t) : x ∈ t :=
  h hx

Element Preservation under Subset Inclusion

Informal description

For any element $x$ of type $\alpha$ and any sets $s, t$ of type $\alpha$, if $x \in s$ and $s \subseteq t$, then $x \in t$.

Set.forall_in_swap theorem

{p : α → β → Prop} : (∀ a ∈ s, ∀ (b), p a b) ↔ ∀ (b), ∀ a ∈ s, p a b

Full source

theorem forall_in_swap {p : α → β → Prop} : (∀ a ∈ s, ∀ (b), p a b) ↔ ∀ (b), ∀ a ∈ s, p a b := by
  tauto

Swapping Universal Quantifiers over Set Membership

Informal description

For any set $s$ of type $\alpha$ and any predicate $p : \alpha \to \beta \to \text{Prop}$, the following are equivalent: 1. For every $a \in s$ and every $b$, $p(a, b)$ holds. 2. For every $b$ and every $a \in s$, $p(a, b)$ holds.

Set.setOf_injective theorem

: Function.Injective (@setOf α)

Full source

theorem setOf_injective : Function.Injective (@setOf α) := injective_id

Injectivity of Set Comprehension

Informal description

The set comprehension function $\{x \mid p x\}$ is injective, meaning that for any two predicates $p, q : \alpha \to \text{Prop}$, if $\{x \mid p x\} = \{x \mid q x\}$ then $p = q$.

Set.setOf_inj theorem

{p q : α → Prop} : {x | p x} = {x | q x} ↔ p = q

Full source

theorem setOf_inj {p q : α → Prop} : { x | p x }{ x | p x } = { x | q x } ↔ p = q := Iff.rfl

Equality of Set Comprehension Predicates

Informal description

For any two predicates $p, q : \alpha \to \text{Prop}$, the set $\{x \mid p x\}$ is equal to $\{x \mid q x\}$ if and only if $p = q$.

Set.mem_setOf theorem

{a : α} {p : α → Prop} : a ∈ {x | p x} ↔ p a

Full source

theorem mem_setOf {a : α} {p : α → Prop} : a ∈ { x | p x }a ∈ { x | p x } ↔ p a :=
  Iff.rfl

Membership in Set Comprehension: $a \in \{x \mid p x\} \leftrightarrow p(a)$

Informal description

For any element $a$ of type $\alpha$ and any predicate $p : \alpha \to \text{Prop}$, the element $a$ belongs to the set $\{x \mid p x\}$ if and only if $p(a)$ holds.

Membership.mem.out theorem

{p : α → Prop} {a : α} (h : a ∈ {x | p x}) : p a

Full source

/-- 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 _root_.Membership.mem.out {p : α → Prop} {a : α} (h : a ∈ { x | p x }) : p a :=
  h

Membership in Set Comprehension Implies Predicate Holds

Informal description

For any predicate $p : \alpha \to \text{Prop}$ and any element $a \in \alpha$, if $a$ belongs to the set $\{x \mid p x\}$, then $p(a)$ holds.

Set.nmem_setOf_iff theorem

{a : α} {p : α → Prop} : a ∉ {x | p x} ↔ ¬p a

Full source

theorem nmem_setOf_iff {a : α} {p : α → Prop} : a ∉ { x | p x }a ∉ { x | p x } ↔ ¬p a :=
  Iff.rfl

Negation of Membership in Set Comprehension: $a \notin \{x \mid p x\} \leftrightarrow \neg p a$

Informal description

For any element $a$ of type $\alpha$ and any predicate $p : \alpha \to \text{Prop}$, the statement $a \notin \{x \mid p x\}$ is equivalent to $\neg p a$.

Set.setOf_mem_eq theorem

{s : Set α} : {x | x ∈ s} = s

Full source

@[simp]
theorem setOf_mem_eq {s : Set α} : { x | x ∈ s } = s :=
  rfl

Set Comprehension Identity: $\{x \mid x \in s\} = s$

Informal description

For any set $s$ of type $\alpha$, the set $\{x \mid x \in s\}$ is equal to $s$ itself.

Set.setOf_set theorem

{s : Set α} : setOf s = s

Full source

theorem setOf_set {s : Set α} : setOf s = s :=
  rfl

Set Comprehension Identity: $\{x \mid x \in s\} = s$

Informal description

For any set $s$ of type $\alpha$, the set comprehension $\{x \mid x \in s\}$ is equal to $s$ itself.

Set.setOf_app_iff theorem

{p : α → Prop} {x : α} : {x | p x} x ↔ p x

Full source

theorem setOf_app_iff {p : α → Prop} {x : α} : { x | p x }{ x | p x } x ↔ p x :=
  Iff.rfl

Membership in Set Comprehension: $x \in \{y \mid p y\} \leftrightarrow p x$

Informal description

For any predicate $p : \alpha \to \text{Prop}$ and any element $x$ of type $\alpha$, the statement $x \in \{y \mid p y\}$ holds if and only if $p x$ holds.

Set.mem_def theorem

{a : α} {s : Set α} : a ∈ s ↔ s a

Full source

theorem mem_def {a : α} {s : Set α} : a ∈ sa ∈ s ↔ s a :=
  Iff.rfl

Membership Definition: $a \in s \leftrightarrow s(a)$

Informal description

For any element $a$ of type $\alpha$ and any set $s$ of type $\alpha$, the statement $a \in s$ holds if and only if the predicate $s$ holds at $a$.

Set.setOf_bijective theorem

: Bijective (setOf : (α → Prop) → Set α)

Full source

theorem setOf_bijective : Bijective (setOf : (α → Prop) → Set α) :=
  bijective_id

Bijectivity of the Set Comprehension Function

Informal description

The function `setOf` that maps predicates $p : \alpha \to \text{Prop}$ to sets $\{x \mid p x\}$ is bijective. That is, it is both injective (distinct predicates yield distinct sets) and surjective (every set can be represented as $\{x \mid p x\}$ for some predicate $p$).

Set.subset_setOf theorem

{p : α → Prop} {s : Set α} : s ⊆ setOf p ↔ ∀ x, x ∈ s → p x

Full source

theorem subset_setOf {p : α → Prop} {s : Set α} : s ⊆ setOf ps ⊆ setOf p ↔ ∀ x, x ∈ s → p x :=
  Iff.rfl

Subset Relation to Set Comprehension: $s \subseteq \{x \mid p x\} \leftrightarrow \forall x \in s, p x$

Informal description

For any predicate $p : \alpha \to \text{Prop}$ and any set $s \subseteq \alpha$, the subset relation $s \subseteq \{x \mid p x\}$ holds if and only if for every element $x \in s$, the predicate $p(x)$ is satisfied.

Set.setOf_subset theorem

{p : α → Prop} {s : Set α} : setOf p ⊆ s ↔ ∀ x, p x → x ∈ s

Full source

theorem setOf_subset {p : α → Prop} {s : Set α} : setOfsetOf p ⊆ ssetOf p ⊆ s ↔ ∀ x, p x → x ∈ s :=
  Iff.rfl

Subset Relation for Set Comprehension: $\{x \mid p(x)\} \subseteq s \leftrightarrow \forall x, p(x) \to x \in s$

Informal description

For any predicate $p : \alpha \to \text{Prop}$ and any set $s : \text{Set } \alpha$, the set $\{x \mid p(x)\}$ is a subset of $s$ if and only if for every element $x$, if $p(x)$ holds then $x$ belongs to $s$.

Set.setOf_subset_setOf theorem

{p q : α → Prop} : {a | p a} ⊆ {a | q a} ↔ ∀ a, p a → q a

Full source

@[simp]
theorem setOf_subset_setOf {p q : α → Prop} : { a | p a }{ a | p a } ⊆ { a | q a }{ a | p a } ⊆ { a | q a } ↔ ∀ a, p a → q a :=
  Iff.rfl

Subset Relation for Set Comprehensions via Implication

Informal description

For any predicates $p, q : \alpha \to \text{Prop}$, the set $\{x \mid p(x)\}$ is a subset of $\{x \mid q(x)\}$ if and only if for every element $x$ of type $\alpha$, $p(x)$ implies $q(x)$. In other words, $$\{x \mid p(x)\} \subseteq \{x \mid q(x)\} \iff \forall x, p(x) \to q(x).$$

Set.setOf_and theorem

{p q : α → Prop} : {a | p a ∧ q a} = {a | p a} ∩ {a | q a}

Full source

theorem setOf_and {p q : α → Prop} : { a | p a ∧ q a } = { a | p a }{ a | p a } ∩ { a | q a } :=
  rfl

Intersection of Set Comprehensions via Logical And

Informal description

For any predicates $p, q : \alpha \to \text{Prop}$, the set of elements satisfying both $p$ and $q$ is equal to the intersection of the sets of elements satisfying $p$ and $q$ respectively. That is, $$\{x \mid p(x) \land q(x)\} = \{x \mid p(x)\} \cap \{x \mid q(x)\}.$$

Set.setOf_or theorem

{p q : α → Prop} : {a | p a ∨ q a} = {a | p a} ∪ {a | q a}

Full source

theorem setOf_or {p q : α → Prop} : { a | p a ∨ q a } = { a | p a }{ a | p a } ∪ { a | q a } :=
  rfl

Set Comprehension of Disjunction Equals Union

Informal description

For any predicates $p, q : \alpha \to \text{Prop}$, the set $\{a \mid p(a) \lor q(a)\}$ is equal to the union $\{a \mid p(a)\} \cup \{a \mid q(a)\}$.

Set.instIsReflSubset instance

: IsRefl (Set α) (· ⊆ ·)

Full source

instance : IsRefl (Set α) (· ⊆ ·) :=
  show IsRefl (Set α) (· ≤ ·) by infer_instance

Reflexivity of Subset Relation on Sets

Informal description

The subset relation $\subseteq$ on sets over a type $\alpha$ is reflexive. That is, for any set $s \subseteq \alpha$, we have $s \subseteq s$.

Set.instIsTransSubset instance

: IsTrans (Set α) (· ⊆ ·)

Full source

instance : IsTrans (Set α) (· ⊆ ·) :=
  show IsTrans (Set α) (· ≤ ·) by infer_instance

Transitivity of Subset Inclusion for Sets

Informal description

The subset relation $\subseteq$ on sets over any type $\alpha$ is transitive. That is, for any sets $s, t, u \subseteq \alpha$, if $s \subseteq t$ and $t \subseteq u$, then $s \subseteq u$.

Set.instTransSubset instance

: Trans ((· ⊆ ·) : Set α → Set α → Prop) (· ⊆ ·) (· ⊆ ·)

Full source

instance : Trans ((· ⊆ ·) : Set α → Set α → Prop) (· ⊆ ·) (· ⊆ ·) :=
  show Trans (· ≤ ·) (· ≤ ·) (· ≤ ·) by infer_instance

Transitivity of Subset Relation on Sets

Informal description

For any type $\alpha$, the subset relation $\subseteq$ on sets over $\alpha$ is transitive. That is, for any sets $s, t, u \subseteq \alpha$, if $s \subseteq t$ and $t \subseteq u$, then $s \subseteq u$.

Set.instIsAntisymmSubset instance

: IsAntisymm (Set α) (· ⊆ ·)

Full source

instance : IsAntisymm (Set α) (· ⊆ ·) :=
  show IsAntisymm (Set α) (· ≤ ·) by infer_instance

Antisymmetry of Subset Inclusion

Informal description

The subset relation $\subseteq$ on sets over any type $\alpha$ is antisymmetric. That is, for any sets $s, t \subseteq \alpha$, if $s \subseteq t$ and $t \subseteq s$, then $s = t$.

Set.instIsIrreflSSubset instance

: IsIrrefl (Set α) (· ⊂ ·)

Full source

instance : IsIrrefl (Set α) (· ⊂ ·) :=
  show IsIrrefl (Set α) (· < ·) by infer_instance

Irreflexivity of Strict Subset Relation on Sets

Informal description

For any type $\alpha$, the strict subset relation $\subset$ on sets over $\alpha$ is irreflexive. That is, for any set $s \subseteq \alpha$, $s \not\subset s$.

Set.instIsTransSSubset instance

: IsTrans (Set α) (· ⊂ ·)

Full source

instance : IsTrans (Set α) (· ⊂ ·) :=
  show IsTrans (Set α) (· < ·) by infer_instance

Transitivity of Strict Subset Relation on Sets

Informal description

The strict subset relation $\subset$ on sets over any type $\alpha$ is transitive. That is, for any sets $s, t, u \subseteq \alpha$, if $s \subset t$ and $t \subset u$, then $s \subset u$.

Set.instTransSSubset instance

: Trans ((· ⊂ ·) : Set α → Set α → Prop) (· ⊂ ·) (· ⊂ ·)

Full source

instance : Trans ((· ⊂ ·) : Set α → Set α → Prop) (· ⊂ ·) (· ⊂ ·) :=
  show Trans (· < ·) (· < ·) (· < ·) by infer_instance

Transitivity of Strict Subset Relation on Sets

Informal description

For any type $\alpha$, the strict subset relation $\subset$ on sets of $\alpha$ is transitive. That is, for any sets $s, t, u \subseteq \alpha$, if $s \subset t$ and $t \subset u$, then $s \subset u$.

Set.instTransSSubsetSubset instance

: Trans ((· ⊂ ·) : Set α → Set α → Prop) (· ⊆ ·) (· ⊂ ·)

Full source

instance : Trans ((· ⊂ ·) : Set α → Set α → Prop) (· ⊆ ·) (· ⊂ ·) :=
  show Trans (· < ·) (· ≤ ·) (· < ·) by infer_instance

Transitivity of Strict Subset with Subset Relation

Informal description

For any type $\alpha$, the strict subset relation $\subset$ on sets is transitive with respect to the subset relation $\subseteq$. That is, for any sets $A, B, C \subseteq \alpha$, if $A \subset B$ and $B \subseteq C$, then $A \subset C$.

Set.instTransSubsetSSubset instance

: Trans ((· ⊆ ·) : Set α → Set α → Prop) (· ⊂ ·) (· ⊂ ·)

Full source

instance : Trans ((· ⊆ ·) : Set α → Set α → Prop) (· ⊂ ·) (· ⊂ ·) :=
  show Trans (· ≤ ·) (· < ·) (· < ·) by infer_instance

Transitivity of Subset with Strict Subset Relation

Informal description

For any type $\alpha$, the subset relation $\subseteq$ on sets of $\alpha$ is transitive with respect to the strict subset relation $\subset$. That is, for any sets $A, B, C \subseteq \alpha$, if $A \subseteq B$ and $B \subset C$, then $A \subset C$.

Set.instIsAsymmSSubset instance

: IsAsymm (Set α) (· ⊂ ·)

Full source

instance : IsAsymm (Set α) (· ⊂ ·) :=
  show IsAsymm (Set α) (· < ·) by infer_instance

Asymmetry of Strict Subset Relation on Sets

Informal description

The strict subset relation $\subset$ on sets is asymmetric. That is, for any two sets $A$ and $B$ of elements of type $\alpha$, if $A \subset B$ then it is not the case that $B \subset A$.

Set.instIsNonstrictStrictOrderSubsetSSubset instance

: IsNonstrictStrictOrder (Set α) (· ⊆ ·) (· ⊂ ·)

Full source

instance : IsNonstrictStrictOrder (Set α) (· ⊆ ·) (· ⊂ ·) :=
  ⟨fun _ _ => Iff.rfl⟩

Subset Relations Form a Non-strict-strict Order

Informal description

For any type $\alpha$, the subset relation $\subseteq$ and the strict subset relation $\subset$ on sets of $\alpha$ form a non-strict-strict order. That is, $\subseteq$ is reflexive and transitive, $\subset$ is irreflexive and transitive, and $s \subset t$ if and only if $s \subseteq t$ and $s \neq t$.

Set.subset_def theorem

: (s ⊆ t) = ∀ x, x ∈ s → x ∈ t

Full source

theorem subset_def : (s ⊆ t) = ∀ x, x ∈ s → x ∈ t :=
  rfl

Definition of Subset Relation: $s \subseteq t \leftrightarrow \forall x, x \in s \to x \in t$

Informal description

For any two sets $s$ and $t$ of elements of type $\alpha$, the subset relation $s \subseteq t$ holds if and only if every element $x$ in $s$ is also in $t$.

Set.ssubset_def theorem

: (s ⊂ t) = (s ⊆ t ∧ ¬t ⊆ s)

Full source

theorem ssubset_def : (s ⊂ t) = (s ⊆ ts ⊆ t ∧ ¬t ⊆ s) :=
  rfl

Definition of Strict Subset Relation: $s \subset t \leftrightarrow (s \subseteq t \land t \not\subseteq s)$

Informal description

For any two sets $s$ and $t$ of elements of type $\alpha$, the strict subset relation $s \subset t$ holds if and only if $s$ is a subset of $t$ and $t$ is not a subset of $s$, i.e., $s \subset t \leftrightarrow (s \subseteq t \land \neg (t \subseteq s))$.

Set.Subset.refl theorem

(a : Set α) : a ⊆ a

Full source

@[refl]
theorem Subset.refl (a : Set α) : a ⊆ a := fun _ => id

Reflexivity of Subset Relation

Informal description

For any set $a$ over a type $\alpha$, the set $a$ is a subset of itself, i.e., $a \subseteq a$.

Set.Subset.rfl theorem

{s : Set α} : s ⊆ s

Full source

theorem Subset.rfl {s : Set α} : s ⊆ s :=
  Subset.refl s

Reflexivity of Subset Relation

Informal description

For any set $s$ of elements of type $\alpha$, the set $s$ is a subset of itself, i.e., $s \subseteq s$.

Set.Subset.trans theorem

{a b c : Set α} (ab : a ⊆ b) (bc : b ⊆ c) : a ⊆ c

Full source

@[trans]
theorem Subset.trans {a b c : Set α} (ab : a ⊆ b) (bc : b ⊆ c) : a ⊆ c := fun _ h => bc <| ab h

Transitivity of Subset Relation

Informal description

For any sets $a$, $b$, and $c$ of elements of type $\alpha$, if $a$ is a subset of $b$ and $b$ is a subset of $c$, then $a$ is a subset of $c$.

Set.mem_of_eq_of_mem theorem

{x y : α} {s : Set α} (hx : x = y) (h : y ∈ s) : x ∈ s

Full source

@[trans]
theorem mem_of_eq_of_mem {x y : α} {s : Set α} (hx : x = y) (h : y ∈ s) : x ∈ s :=
  hx.symm ▸ h

Membership Preservation under Equality

Informal description

For any elements $x$ and $y$ of type $\alpha$ and any set $s$ of elements of type $\alpha$, if $x = y$ and $y \in s$, then $x \in s$.

Set.Subset.antisymm theorem

{a b : Set α} (h₁ : a ⊆ b) (h₂ : b ⊆ a) : a = b

Full source

theorem Subset.antisymm {a b : Set α} (h₁ : a ⊆ b) (h₂ : b ⊆ a) : a = b :=
  Set.ext fun _ => ⟨@h₁ _, @h₂ _⟩

Antisymmetry of Subset Relation: $a \subseteq b \land b \subseteq a \implies a = b$

Informal description

For any two sets $a$ and $b$ over a type $\alpha$, if $a \subseteq b$ and $b \subseteq a$, then $a = b$.

Set.Subset.antisymm_iff theorem

{a b : Set α} : a = b ↔ a ⊆ b ∧ b ⊆ a

Full source

theorem Subset.antisymm_iff {a b : Set α} : a = b ↔ a ⊆ b ∧ b ⊆ a :=
  ⟨fun e => ⟨e.subset, e.symm.subset⟩, fun ⟨h₁, h₂⟩ => Subset.antisymm h₁ h₂⟩

Set Equality via Mutual Subsets: $a = b \leftrightarrow a \subseteq b \land b \subseteq a$

Informal description

For any two sets $a$ and $b$ over a type $\alpha$, the equality $a = b$ holds if and only if $a$ is a subset of $b$ and $b$ is a subset of $a$, i.e., $a \subseteq b$ and $b \subseteq a$.

Set.mem_of_subset_of_mem theorem

{s₁ s₂ : Set α} {a : α} (h : s₁ ⊆ s₂) : a ∈ s₁ → a ∈ s₂

Full source

theorem mem_of_subset_of_mem {s₁ s₂ : Set α} {a : α} (h : s₁ ⊆ s₂) : a ∈ s₁ → a ∈ s₂ :=
  @h _

Element Preservation under Subset Inclusion

Informal description

For any sets $s₁$ and $s₂$ of type $\alpha$, and any element $a \in \alpha$, if $s₁ \subseteq s₂$ and $a \in s₁$, then $a \in s₂$.

Set.not_mem_subset theorem

(h : s ⊆ t) : a ∉ t → a ∉ s

Full source

theorem not_mem_subset (h : s ⊆ t) : a ∉ t → a ∉ s :=
  mt <| mem_of_subset_of_mem h

Non-membership Preservation under Subset Inclusion

Informal description

For any sets $s$ and $t$ of elements of type $\alpha$, if $s \subseteq t$ and an element $a \notin t$, then $a \notin s$.

Set.not_subset theorem

: ¬s ⊆ t ↔ ∃ a ∈ s, a ∉ t

Full source

theorem not_subset : ¬s ⊆ t¬s ⊆ t ↔ ∃ a ∈ s, a ∉ t := by
  simp only [subset_def, not_forall, exists_prop]

Characterization of Non-Subset Relation

Informal description

For any sets $s$ and $t$ of elements of type $\alpha$, the statement that $s$ is not a subset of $t$ is equivalent to the existence of an element $a \in s$ such that $a \notin t$. In other words, $\neg (s \subseteq t) \leftrightarrow \exists a \in s, a \notin t$.

Set.not_top_subset theorem

: ¬⊤ ⊆ s ↔ ∃ a, a ∉ s

Full source

theorem not_top_subset : ¬⊤ ⊆ s¬⊤ ⊆ s ↔ ∃ a, a ∉ s := by
  simp [not_subset]

Non-Subset Characterization of Universal Set

Informal description

The universal set $\top$ is not a subset of a set $s$ if and only if there exists an element $a$ that is not in $s$. In other words, $\neg (\top \subseteq s) \leftrightarrow \exists a, a \notin s$.

Set.exists_of_ssubset theorem

{s t : Set α} (h : s ⊂ t) : ∃ x ∈ t, x ∉ s

Full source

theorem exists_of_ssubset {s t : Set α} (h : s ⊂ t) : ∃ x ∈ t, x ∉ s :=
  not_subset.1 h.2

Existence of Element in Strict Superset

Informal description

For any sets $s$ and $t$ of elements of type $\alpha$, if $s$ is a strict subset of $t$ (denoted $s \subset t$), then there exists an element $x \in t$ such that $x \notin s$.

Set.ssubset_iff_subset_ne theorem

{s t : Set α} : s ⊂ t ↔ s ⊆ t ∧ s ≠ t

Full source

protected theorem ssubset_iff_subset_ne {s t : Set α} : s ⊂ ts ⊂ t ↔ s ⊆ t ∧ s ≠ t :=
  @lt_iff_le_and_ne (Set α) _ s t

Characterization of Strict Subset via Subset and Inequality

Informal description

For any two sets $s$ and $t$ over a type $\alpha$, the strict subset relation $s \subset t$ holds if and only if $s$ is a subset of $t$ (i.e., $s \subseteq t$) and $s$ is not equal to $t$ (i.e., $s \neq t$).

Set.ssubset_iff_of_subset theorem

{s t : Set α} (h : s ⊆ t) : s ⊂ t ↔ ∃ x ∈ t, x ∉ s

Full source

theorem ssubset_iff_of_subset {s t : Set α} (h : s ⊆ t) : s ⊂ ts ⊂ t ↔ ∃ x ∈ t, x ∉ s :=
  ⟨exists_of_ssubset, fun ⟨_, hxt, hxs⟩ => ⟨h, fun h => hxs <| h hxt⟩⟩

Characterization of Strict Subset via Existence of Non-Member Element

Informal description

For any sets $s$ and $t$ over a type $\alpha$, if $s$ is a subset of $t$ (i.e., $s \subseteq t$), then $s$ is a strict subset of $t$ (i.e., $s \subset t$) if and only if there exists an element $x \in t$ such that $x \notin s$.

Set.ssubset_iff_exists theorem

{s t : Set α} : s ⊂ t ↔ s ⊆ t ∧ ∃ x ∈ t, x ∉ s

Full source

theorem ssubset_iff_exists {s t : Set α} : s ⊂ ts ⊂ t ↔ s ⊆ t ∧ ∃ x ∈ t, x ∉ s :=
  ⟨fun h ↦ ⟨h.le, Set.exists_of_ssubset h⟩, fun ⟨h1, h2⟩ ↦ (Set.ssubset_iff_of_subset h1).mpr h2⟩

Characterization of Strict Subset via Subset and Existence of Non-Member Element

Informal description

For any sets $s$ and $t$ of elements of type $\alpha$, the strict subset relation $s \subset t$ holds if and only if $s$ is a subset of $t$ (i.e., $s \subseteq t$) and there exists an element $x \in t$ such that $x \notin s$.

Set.ssubset_of_ssubset_of_subset theorem

{s₁ s₂ s₃ : Set α} (hs₁s₂ : s₁ ⊂ s₂) (hs₂s₃ : s₂ ⊆ s₃) : s₁ ⊂ s₃

Full source

protected theorem ssubset_of_ssubset_of_subset {s₁ s₂ s₃ : Set α} (hs₁s₂ : s₁ ⊂ s₂)
    (hs₂s₃ : s₂ ⊆ s₃) : s₁ ⊂ s₃ :=
  ⟨Subset.trans hs₁s₂.1 hs₂s₃, fun hs₃s₁ => hs₁s₂.2 (Subset.trans hs₂s₃ hs₃s₁)⟩

Transitivity of Strict Subset Relation via Subset

Informal description

For any sets $s₁, s₂, s₃$ of elements of type $\alpha$, if $s₁$ is a strict subset of $s₂$ and $s₂$ is a subset of $s₃$, then $s₁$ is a strict subset of $s₃$.

Set.ssubset_of_subset_of_ssubset theorem

{s₁ s₂ s₃ : Set α} (hs₁s₂ : s₁ ⊆ s₂) (hs₂s₃ : s₂ ⊂ s₃) : s₁ ⊂ s₃

Full source

protected theorem ssubset_of_subset_of_ssubset {s₁ s₂ s₃ : Set α} (hs₁s₂ : s₁ ⊆ s₂)
    (hs₂s₃ : s₂ ⊂ s₃) : s₁ ⊂ s₃ :=
  ⟨Subset.trans hs₁s₂ hs₂s₃.1, fun hs₃s₁ => hs₂s₃.2 (Subset.trans hs₃s₁ hs₁s₂)⟩

Transitivity of Strict Subset Relation via Subset and Strict Subset

Informal description

For any sets $s_1, s_2, s_3$ of elements of type $\alpha$, if $s_1$ is a subset of $s_2$ and $s_2$ is a strict subset of $s_3$, then $s_1$ is a strict subset of $s_3$.

Set.not_mem_empty theorem

(x : α) : ¬x ∈ (∅ : Set α)

Full source

theorem not_mem_empty (x : α) : ¬x ∈ (∅ : Set α) :=
  id

No Element Belongs to the Empty Set

Informal description

For any element $x$ of type $\alpha$, $x$ does not belong to the empty set $\emptyset$.

Set.not_not_mem theorem

: ¬a ∉ s ↔ a ∈ s

Full source

theorem not_not_mem : ¬a ∉ s¬a ∉ s ↔ a ∈ s :=
  not_not

Double Negation of Membership Equals Membership

Informal description

For any element $a$ and set $s$, the statement "$a$ is not not in $s$" is equivalent to "$a$ is in $s$", i.e., $\neg (a \notin s) \leftrightarrow a \in s$.

Set.nonempty_coe_sort theorem

{s : Set α} : Nonempty ↥s ↔ s.Nonempty

Full source

theorem nonempty_coe_sort {s : Set α} : NonemptyNonempty ↥s ↔ s.Nonempty :=
  nonempty_subtype

Nonempty Subtype Characterization for Sets

Informal description

For any set $s$ of elements of type $\alpha$, the subtype corresponding to $s$ is nonempty if and only if $s$ itself is nonempty.

Set.nonempty_def theorem

: s.Nonempty ↔ ∃ x, x ∈ s

Full source

theorem nonempty_def : s.Nonempty ↔ ∃ x, x ∈ s :=
  Iff.rfl

Characterization of Nonempty Sets

Informal description

A set $s$ is nonempty if and only if there exists an element $x$ such that $x \in s$.

Set.nonempty_of_mem theorem

{x} (h : x ∈ s) : s.Nonempty

Full source

theorem nonempty_of_mem {x} (h : x ∈ s) : s.Nonempty :=
  ⟨x, h⟩

Nonempty Set from Membership

Informal description

For any element $x$ in a set $s$, the set $s$ is nonempty.

Set.Nonempty.not_subset_empty theorem

: s.Nonempty → ¬s ⊆ ∅

Full source

theorem Nonempty.not_subset_empty : s.Nonempty → ¬s ⊆ ∅
  | ⟨_, hx⟩, hs => hs hx

Nonempty sets are not subsets of the empty set

Informal description

If a set $s$ is nonempty, then it is not a subset of the empty set.

Set.Nonempty.some definition

(h : s.Nonempty) : α

Full source

/-- 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. -/
protected noncomputable def Nonempty.some (h : s.Nonempty) : α :=
  Classical.choose h

Witness of a nonempty set

Informal description

Given a nonempty set $s$ over a type $\alpha$, this function returns a witness element in $\alpha$ that belongs to $s$. The witness is obtained using the axiom of choice.

Set.Nonempty.some_mem theorem

(h : s.Nonempty) : h.some ∈ s

Full source

protected theorem Nonempty.some_mem (h : s.Nonempty) : h.some ∈ s :=
  Classical.choose_spec h

Witness Element Belongs to Nonempty Set

Informal description

For any nonempty set $s$ over a type $\alpha$, the witness element $h.\text{some}$ obtained from the nonempty condition $h : s.\text{Nonempty}$ satisfies $h.\text{some} \in s$.

Set.Nonempty.mono theorem

(ht : s ⊆ t) (hs : s.Nonempty) : t.Nonempty

Full source

theorem Nonempty.mono (ht : s ⊆ t) (hs : s.Nonempty) : t.Nonempty :=
  hs.imp ht

Nonempty Subset Implies Nonempty Superset

Informal description

If $s$ is a nonempty subset of $t$ (i.e., $s \subseteq t$ and $s \neq \emptyset$), then $t$ is also nonempty.

Set.nonempty_of_not_subset theorem

(h : ¬s ⊆ t) : (s \ t).Nonempty

Full source

theorem nonempty_of_not_subset (h : ¬s ⊆ t) : (s \ t).Nonempty :=
  let ⟨x, xs, xt⟩ := not_subset.1 h
  ⟨x, xs, xt⟩

Nonemptiness of Set Difference from Non-Subset Condition

Informal description

For any sets $s$ and $t$ of elements of type $\alpha$, if $s$ is not a subset of $t$ (i.e., $\neg (s \subseteq t)$), then the set difference $s \setminus t$ is nonempty.

Set.nonempty_of_ssubset theorem

(ht : s ⊂ t) : (t \ s).Nonempty

Full source

theorem nonempty_of_ssubset (ht : s ⊂ t) : (t \ s).Nonempty :=
  nonempty_of_not_subset ht.2

Nonemptiness of Set Difference under Strict Subset Relation

Informal description

For any sets $s$ and $t$ of elements of type $\alpha$, if $s$ is a strict subset of $t$ (i.e., $s \subset t$), then the set difference $t \setminus s$ is nonempty.

Set.Nonempty.of_diff theorem

(h : (s \ t).Nonempty) : s.Nonempty

Full source

theorem Nonempty.of_diff (h : (s \ t).Nonempty) : s.Nonempty :=
  h.imp fun _ => And.left

Nonemptiness of Set Difference Implies Nonemptiness of Original Set

Informal description

If the set difference $s \setminus t$ is nonempty, then the set $s$ is nonempty.

Set.nonempty_of_ssubset' theorem

(ht : s ⊂ t) : t.Nonempty

Full source

theorem nonempty_of_ssubset' (ht : s ⊂ t) : t.Nonempty :=
  (nonempty_of_ssubset ht).of_diff

Nonemptiness of Superset under Strict Subset Relation

Informal description

For any sets $s$ and $t$ over a type $\alpha$, if $s$ is a strict subset of $t$ (i.e., $s \subset t$), then $t$ is nonempty.

Set.Nonempty.inl theorem

(hs : s.Nonempty) : (s ∪ t).Nonempty

Full source

theorem Nonempty.inl (hs : s.Nonempty) : (s ∪ t).Nonempty :=
  hs.imp fun _ => Or.inl

Nonempty set implies nonempty union (left variant)

Informal description

If a set $s$ is nonempty, then the union $s \cup t$ is also nonempty for any set $t$.

Set.Nonempty.inr theorem

(ht : t.Nonempty) : (s ∪ t).Nonempty

Full source

theorem Nonempty.inr (ht : t.Nonempty) : (s ∪ t).Nonempty :=
  ht.imp fun _ => Or.inr

Nonempty set implies nonempty union on the right

Informal description

For any sets $s$ and $t$ over a type $\alpha$, if $t$ is nonempty, then the union $s \cup t$ is also nonempty.

Set.union_nonempty theorem

: (s ∪ t).Nonempty ↔ s.Nonempty ∨ t.Nonempty

Full source

@[simp]
theorem union_nonempty : (s ∪ t).Nonempty ↔ s.Nonempty ∨ t.Nonempty :=
  exists_or

Nonempty Union Characterization: $s \cup t \neq \emptyset \leftrightarrow s \neq \emptyset \lor t \neq \emptyset$

Informal description

For any two sets $s$ and $t$ over a type $\alpha$, the union $s \cup t$ is nonempty if and only if at least one of $s$ or $t$ is nonempty.

Set.Nonempty.left theorem

(h : (s ∩ t).Nonempty) : s.Nonempty

Full source

theorem Nonempty.left (h : (s ∩ t).Nonempty) : s.Nonempty :=
  h.imp fun _ => And.left

Nonempty Intersection Implies Nonempty Left Set

Informal description

For any sets $s$ and $t$ over a type $\alpha$, if the intersection $s \cap t$ is nonempty, then $s$ is nonempty.

Set.Nonempty.right theorem

(h : (s ∩ t).Nonempty) : t.Nonempty

Full source

theorem Nonempty.right (h : (s ∩ t).Nonempty) : t.Nonempty :=
  h.imp fun _ => And.right

Nonempty Intersection Implies Nonempty Right Set

Informal description

For any sets $s$ and $t$ over a type $\alpha$, if the intersection $s \cap t$ is nonempty, then $t$ is nonempty.

Set.inter_nonempty theorem

: (s ∩ t).Nonempty ↔ ∃ x, x ∈ s ∧ x ∈ t

Full source

theorem inter_nonempty : (s ∩ t).Nonempty ↔ ∃ x, x ∈ s ∧ x ∈ t :=
  Iff.rfl

Nonempty Intersection Characterization

Informal description

The intersection of two sets $s$ and $t$ is nonempty if and only if there exists an element $x$ that belongs to both $s$ and $t$, i.e., $s \cap t \neq \emptyset \leftrightarrow \exists x, x \in s \land x \in t$.

Set.inter_nonempty_iff_exists_left theorem

: (s ∩ t).Nonempty ↔ ∃ x ∈ s, x ∈ t

Full source

theorem inter_nonempty_iff_exists_left : (s ∩ t).Nonempty ↔ ∃ x ∈ s, x ∈ t := by
  simp_rw [inter_nonempty]

Nonempty Intersection Characterization via Common Element

Informal description

The intersection of two sets $s$ and $t$ is nonempty if and only if there exists an element $x$ such that $x \in s$ and $x \in t$.

Set.inter_nonempty_iff_exists_right theorem

: (s ∩ t).Nonempty ↔ ∃ x ∈ t, x ∈ s

Full source

theorem inter_nonempty_iff_exists_right : (s ∩ t).Nonempty ↔ ∃ x ∈ t, x ∈ s := by
  simp_rw [inter_nonempty, and_comm]

Nonempty Intersection Criterion via Right Set Membership

Informal description

The intersection of two sets $s$ and $t$ is nonempty if and only if there exists an element $x$ in $t$ that also belongs to $s$.

Set.nonempty_iff_univ_nonempty theorem

: Nonempty α ↔ (univ : Set α).Nonempty

Full source

theorem nonempty_iff_univ_nonempty : NonemptyNonempty α ↔ (univ : Set α).Nonempty :=
  ⟨fun ⟨x⟩ => ⟨x, trivial⟩, fun ⟨x, _⟩ => ⟨x⟩⟩

Nonemptiness of Type and Universal Set

Informal description

A type $\alpha$ is nonempty if and only if the universal set $\text{univ} : \text{Set } \alpha$ is nonempty.

Set.univ_nonempty theorem

: ∀ [Nonempty α], (univ : Set α).Nonempty

Full source

@[simp]
theorem univ_nonempty : ∀ [Nonempty α], (univ : Set α).Nonempty
  | ⟨x⟩ => ⟨x, trivial⟩

Nonemptiness of the Universal Set for Nonempty Types

Informal description

For any nonempty type $\alpha$, the universal set $\text{univ} : \text{Set } \alpha$ is nonempty.

Set.Nonempty.to_subtype theorem

: s.Nonempty → Nonempty (↥s)

Full source

theorem Nonempty.to_subtype : s.Nonempty → Nonempty (↥s) :=
  nonempty_subtype.2

Nonempty Set Implies Nonempty Subtype

Informal description

For any set $s$ of type $\alpha$, if $s$ is nonempty (i.e., there exists an element $x \in s$), then the subtype corresponding to $s$ is also nonempty.

Set.Nonempty.to_type theorem

: s.Nonempty → Nonempty α

Full source

theorem Nonempty.to_type : s.Nonempty → Nonempty α := fun ⟨x, _⟩ => ⟨x⟩

Nonempty Set Implies Nonempty Type

Informal description

If a set $s$ over a type $\alpha$ is nonempty (i.e., there exists an element $x \in s$), then the type $\alpha$ itself is nonempty.

Set.univ.nonempty instance

[Nonempty α] : Nonempty (↥(Set.univ : Set α))

Full source

instance univ.nonempty [Nonempty α] : Nonempty (↥(Set.univ : Set α)) :=
  Set.univ_nonempty.to_subtype

Nonemptiness of the Universal Set Subtype

Informal description

For any nonempty type $\alpha$, the universal set $\text{univ} : \text{Set } \alpha$ is nonempty when viewed as a subtype.

Set.instNonemptyTop instance

[Nonempty α] : Nonempty (⊤ : Set α)

Full source

instance instNonemptyTop [Nonempty α] : Nonempty (⊤ : Set α) :=
  inferInstanceAs (Nonempty (univ : Set α))

Nonemptiness of the Universal Set

Informal description

For any nonempty type $\alpha$, the universal set $\top$ (which is the set of all elements of $\alpha$) is nonempty.

Set.Nonempty.of_subtype theorem

[Nonempty (↥s)] : s.Nonempty

Full source

theorem Nonempty.of_subtype [Nonempty (↥s)] : s.Nonempty := nonempty_subtype.mp ‹_›

Nonempty Subtype Implies Nonempty Set

Informal description

If the subtype corresponding to a set $s$ is nonempty, then $s$ itself is nonempty.

Set.empty_def theorem

: (∅ : Set α) = {_x : α | False}

Full source

theorem empty_def : (∅ : Set α) = { _x : α | False } :=
  rfl

Definition of the Empty Set via False Predicate

Informal description

The empty set $\emptyset$ is equal to the set of all elements $x$ of type $\alpha$ satisfying the false predicate, i.e., $\emptyset = \{x \mid \text{False}\}$.

Set.mem_empty_iff_false theorem

(x : α) : x ∈ (∅ : Set α) ↔ False

Full source

@[simp]
theorem mem_empty_iff_false (x : α) : x ∈ (∅ : Set α)x ∈ (∅ : Set α) ↔ False :=
  Iff.rfl

Membership in Empty Set is False

Informal description

For any element $x$ of type $\alpha$, the statement $x \in \emptyset$ is equivalent to false.

Set.setOf_false theorem

: {_a : α | False} = ∅

Full source

@[simp]
theorem setOf_false : { _a : α | False } = ∅ :=
  rfl

Empty Set Construction from False Predicate

Informal description

The set of all elements $x$ of type $\alpha$ satisfying the false predicate is equal to the empty set, i.e., $\{x \mid \text{False}\} = \emptyset$.

Set.setOf_bot theorem

: {_x : α | ⊥} = ∅

Full source

@[simp] theorem setOf_bot : { _x : α | ⊥ } = ∅ := rfl

Empty Set Construction from False Proposition

Informal description

The set of all elements $x$ of type $\alpha$ satisfying the false proposition $\bot$ is equal to the empty set, i.e., $\{x \mid \bot\} = \emptyset$.

Set.empty_subset theorem

(s : Set α) : ∅ ⊆ s

Full source

@[simp]
theorem empty_subset (s : Set α) : ∅∅ ⊆ s :=
  nofun

Empty Set is Subset of Any Set

Informal description

For any set $s$ of elements of type $\alpha$, the empty set is a subset of $s$, i.e., $\emptyset \subseteq s$.

Set.subset_empty_iff theorem

{s : Set α} : s ⊆ ∅ ↔ s = ∅

Full source

@[simp]
theorem subset_empty_iff {s : Set α} : s ⊆ ∅s ⊆ ∅ ↔ s = ∅ :=
  (Subset.antisymm_iff.trans <| and_iff_left (empty_subset _)).symm

Subset of Empty Set is Empty

Informal description

For any set $s$ of elements of type $\alpha$, $s$ is a subset of the empty set if and only if $s$ is equal to the empty set, i.e., $s \subseteq \emptyset \leftrightarrow s = \emptyset$.

Set.uniqueEmpty instance

[IsEmpty α] : Unique (Set α)

Full source

/-- There is exactly one set of a type that is empty. -/
instance uniqueEmpty [IsEmpty α] : Unique (Set α) where
  default := ∅
  uniq := eq_empty_of_isEmpty

Uniqueness of the Empty Set for Empty Types

Informal description

For any empty type $\alpha$, the collection of sets over $\alpha$ has exactly one element, namely the empty set.

Set.not_nonempty_iff_eq_empty theorem

{s : Set α} : ¬s.Nonempty ↔ s = ∅

Full source

/-- See also `Set.nonempty_iff_ne_empty`. -/
theorem not_nonempty_iff_eq_empty {s : Set α} : ¬s.Nonempty¬s.Nonempty ↔ s = ∅ := by
  simp only [Set.Nonempty, not_exists, eq_empty_iff_forall_not_mem]

Equivalence of Non-emptiness and Non-empty Set Condition

Informal description

For any set $s$ of type $\alpha$, the set $s$ is empty if and only if it is not nonempty, i.e., $\neg (\text{Nonempty } s) \leftrightarrow s = \emptyset$.

Set.nonempty_iff_ne_empty theorem

: s.Nonempty ↔ s ≠ ∅

Full source

/-- See also `Set.not_nonempty_iff_eq_empty`. -/
theorem nonempty_iff_ne_empty : s.Nonempty ↔ s ≠ ∅ :=
  not_nonempty_iff_eq_empty.not_right

Nonempty Set Characterization: $s \neq \emptyset$

Informal description

A set $s$ is nonempty if and only if it is not equal to the empty set, i.e., $s \neq \emptyset$.

Set.not_nonempty_iff_eq_empty' theorem

: ¬Nonempty s ↔ s = ∅

Full source

/-- See also `nonempty_iff_ne_empty'`. -/
theorem not_nonempty_iff_eq_empty' : ¬Nonempty s¬Nonempty s ↔ s = ∅ := by
  rw [nonempty_subtype, not_exists, eq_empty_iff_forall_not_mem]

Empty Set Characterization via Non-emptiness

Informal description

For any set $s$ of type $\alpha$, the set $s$ is empty if and only if its corresponding subtype is non-inhabited. In other words, $\neg (\text{Nonempty } s) \leftrightarrow s = \emptyset$.

Set.nonempty_iff_ne_empty' theorem

: Nonempty s ↔ s ≠ ∅

Full source

/-- See also `not_nonempty_iff_eq_empty'`. -/
theorem nonempty_iff_ne_empty' : NonemptyNonempty s ↔ s ≠ ∅ :=
  not_nonempty_iff_eq_empty'.not_right

Nonempty Set Characterization: $\text{Nonempty } s \leftrightarrow s \neq \emptyset$

Informal description

A set $s$ is nonempty if and only if it is not equal to the empty set, i.e., $\text{Nonempty } s \leftrightarrow s \neq \emptyset$.

Set.not_nonempty_empty theorem

: ¬(∅ : Set α).Nonempty

Full source

@[simp]
theorem not_nonempty_empty : ¬(∅ : Set α).Nonempty := fun ⟨_, hx⟩ => hx

Empty Set is Not Nonempty

Informal description

The empty set $\emptyset$ over any type $\alpha$ is not nonempty, i.e., $\neg (\text{Nonempty } \emptyset)$.

Set.isEmpty_coe_sort theorem

{s : Set α} : IsEmpty (↥s) ↔ s = ∅

Full source

@[simp]
theorem isEmpty_coe_sort {s : Set α} : IsEmptyIsEmpty (↥s) ↔ s = ∅ :=
  not_iff_not.1 <| by simpa using nonempty_iff_ne_empty

Empty Subtype Characterization: $\text{IsEmpty}(s) \leftrightarrow s = \emptyset$

Informal description

For any set $s$ of type $\alpha$, the subtype corresponding to $s$ is empty if and only if $s$ is equal to the empty set. In other words, $\text{IsEmpty} (s : \text{Type}) \leftrightarrow s = \emptyset$.

Set.subset_eq_empty theorem

{s t : Set α} (h : t ⊆ s) (e : s = ∅) : t = ∅

Full source

theorem subset_eq_empty {s t : Set α} (h : t ⊆ s) (e : s = ∅) : t = ∅ :=
  subset_empty_iff.1 <| e ▸ h

Subset of Empty Set is Empty

Informal description

For any sets $s$ and $t$ of elements of type $\alpha$, if $t$ is a subset of $s$ and $s$ is equal to the empty set, then $t$ is also equal to the empty set. In other words, $t \subseteq s \land s = \emptyset \implies t = \emptyset$.

Set.forall_mem_empty theorem

{p : α → Prop} : (∀ x ∈ (∅ : Set α), p x) ↔ True

Full source

theorem forall_mem_empty {p : α → Prop} : (∀ x ∈ (∅ : Set α), p x) ↔ True :=
  iff_true_intro fun _ => False.elim

Universal Quantification over the Empty Set is Trivially True

Informal description

For any predicate $p$ on elements of type $\alpha$, the statement "for all $x$ in the empty set, $p(x)$ holds" is equivalent to the true proposition.

Set.instIsEmptyElemEmptyCollection instance

(α : Type u) : IsEmpty.{u + 1} (↥(∅ : Set α))

Full source

instance (α : Type u) : IsEmpty.{u + 1} (↥(∅ : Set α)) :=
  ⟨fun x => x.2⟩

Empty Set as Empty Type

Informal description

For any type $\alpha$, the empty set $\emptyset$ as a subtype is an empty type, meaning it has no elements.

Set.empty_ssubset theorem

: ∅ ⊂ s ↔ s.Nonempty

Full source

@[simp]
theorem empty_ssubset : ∅∅ ⊂ s∅ ⊂ s ↔ s.Nonempty :=
  (@bot_lt_iff_ne_bot (Set α) _ _ _).trans nonempty_iff_ne_empty.symm

Empty Set is Strict Subset if and only if Set is Nonempty

Informal description

For any set $s$ over a type $\alpha$, the empty set $\emptyset$ is a strict subset of $s$ if and only if $s$ is nonempty, i.e., $\emptyset \subset s \leftrightarrow s \neq \emptyset$.

Set.setOf_true theorem

: {_x : α | True} = univ

Full source

@[simp]
theorem setOf_true : { _x : α | True } = univ :=
  rfl

Universal Set as Set of All Elements Satisfying True

Informal description

The set of all elements $x$ of type $\alpha$ satisfying the condition "True" is equal to the universal set on $\alpha$, i.e., $\{x \mid \text{True}\} = \text{univ}$.

Set.setOf_top theorem

: {_x : α | ⊤} = univ

Full source

@[simp] theorem setOf_top : { _x : α | ⊤ } = univ := rfl

Set of All Elements Satisfying True Equals Universal Set

Informal description

The set of all elements $x$ of type $\alpha$ satisfying the true proposition $\top$ is equal to the universal set $\text{univ}$ on $\alpha$, i.e., $\{x \mid \top\} = \text{univ}$.

Set.univ_eq_empty_iff theorem

: (univ : Set α) = ∅ ↔ IsEmpty α

Full source

@[simp]
theorem univ_eq_empty_iff : (univ : Set α) = ∅ ↔ IsEmpty α :=
  eq_empty_iff_forall_not_mem.trans
    ⟨fun H => ⟨fun x => H x trivial⟩, fun H x _ => @IsEmpty.false α H x⟩

Universal Set Equals Empty Set iff Type is Empty

Informal description

The universal set on a type $\alpha$ is equal to the empty set if and only if the type $\alpha$ is empty, i.e., $\text{univ} = \emptyset \leftrightarrow \text{IsEmpty}(\alpha)$.

Set.empty_ne_univ theorem

[Nonempty α] : (∅ : Set α) ≠ univ

Full source

theorem empty_ne_univ [Nonempty α] : (∅ : Set α) ≠ univ := fun e =>
  not_isEmpty_of_nonempty α <| univ_eq_empty_iff.1 e.symm

Empty Set Not Equal to Universal Set in Nonempty Types

Informal description

For any nonempty type $\alpha$, the empty set $\emptyset$ is not equal to the universal set $\text{univ}$ (the set containing all elements of $\alpha$).

Set.subset_univ theorem

(s : Set α) : s ⊆ univ

Full source

@[simp]
theorem subset_univ (s : Set α) : s ⊆ univ := fun _ _ => trivial

Every Set is a Subset of the Universal Set

Informal description

For any set $s$ of elements of type $\alpha$, $s$ is a subset of the universal set $\text{univ}$ (the set containing all elements of $\alpha$).

Set.univ_subset_iff theorem

{s : Set α} : univ ⊆ s ↔ s = univ

Full source

@[simp]
theorem univ_subset_iff {s : Set α} : univuniv ⊆ suniv ⊆ s ↔ s = univ :=
  @top_le_iff _ _ _ s

Universal Set Subset Characterization: $\text{univ} \subseteq s \leftrightarrow s = \text{univ}$

Informal description

For any set $s$ of elements of type $\alpha$, the universal set $\text{univ}$ is a subset of $s$ if and only if $s$ is equal to $\text{univ}$.

Set.exists_mem_of_nonempty theorem

(α) : ∀ [Nonempty α], ∃ x : α, x ∈ (univ : Set α)

Full source

theorem exists_mem_of_nonempty (α) : ∀ [Nonempty α], ∃ x : α, x ∈ (univ : Set α)
  | ⟨x⟩ => ⟨x, trivial⟩

Existence of Element in Universal Set for Nonempty Types

Informal description

For any nonempty type $\alpha$, there exists an element $x \in \alpha$ that belongs to the universal set (i.e., $x$ satisfies the trivial predicate $\text{True}$).

Set.ne_univ_iff_exists_not_mem theorem

{α : Type*} (s : Set α) : s ≠ univ ↔ ∃ a, a ∉ s

Full source

theorem ne_univ_iff_exists_not_mem {α : Type*} (s : Set α) : s ≠ univs ≠ univ ↔ ∃ a, a ∉ s := by
  rw [← not_forall, ← eq_univ_iff_forall]

Characterization of Non-Universal Sets via Non-Membership

Informal description

For any set $s$ of elements of type $\alpha$, $s$ is not equal to the universal set if and only if there exists an element $a \in \alpha$ such that $a \notin s$.

Set.not_subset_iff_exists_mem_not_mem theorem

{α : Type*} {s t : Set α} : ¬s ⊆ t ↔ ∃ x, x ∈ s ∧ x ∉ t

Full source

theorem not_subset_iff_exists_mem_not_mem {α : Type*} {s t : Set α} :
    ¬s ⊆ t¬s ⊆ t ↔ ∃ x, x ∈ s ∧ x ∉ t := by simp [subset_def]

Characterization of Non-Subset via Existence of Non-Member Element

Informal description

For any two sets $s$ and $t$ of elements of type $\alpha$, $s$ is not a subset of $t$ if and only if there exists an element $x \in \alpha$ such that $x \in s$ and $x \notin t$.

Set.univ_unique theorem

[Unique α] : @Set.univ α = { default }

Full source

theorem univ_unique [Unique α] : @Set.univ α = {default} :=
  Set.ext fun x => iff_of_true trivial <| Subsingleton.elim x default

Universal Set Equals Singleton for Unique Types

Informal description

For a type $\alpha$ with a unique element (denoted as `default`), the universal set `univ` is equal to the singleton set containing `default`, i.e., $\text{univ} = \{\text{default}\}$.

Set.ssubset_univ_iff theorem

: s ⊂ univ ↔ s ≠ univ

Full source

theorem ssubset_univ_iff : s ⊂ univs ⊂ univ ↔ s ≠ univ :=
  lt_top_iff_ne_top

Characterization of Strict Subset of Universal Set: $s \subset \text{univ} \leftrightarrow s \neq \text{univ}$

Informal description

For any set $s$ of elements of type $\alpha$, $s$ is a strict subset of the universal set $\text{univ}$ if and only if $s$ is not equal to $\text{univ}$.

Set.nontrivial_of_nonempty instance

[Nonempty α] : Nontrivial (Set α)

Full source

instance nontrivial_of_nonempty [Nonempty α] : Nontrivial (Set α) :=
  ⟨⟨∅, univ, empty_ne_univ⟩⟩

Nontriviality of Power Set for Nonempty Types

Informal description

For any nonempty type $\alpha$, the collection of all subsets of $\alpha$ is a nontrivial type, meaning it contains at least two distinct sets.

Set.union_def theorem

{s₁ s₂ : Set α} : s₁ ∪ s₂ = {a | a ∈ s₁ ∨ a ∈ s₂}

Full source

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

Definition of Set Union via Membership Condition

Informal description

For any two sets $s_1$ and $s_2$ of type $\alpha$, their union $s_1 \cup s_2$ is equal to the set $\{a \mid a \in s_1 \lor a \in s_2\}$.

Set.mem_union_left theorem

{x : α} {a : Set α} (b : Set α) : x ∈ a → x ∈ a ∪ b

Full source

theorem mem_union_left {x : α} {a : Set α} (b : Set α) : x ∈ a → x ∈ a ∪ b :=
  Or.inl

Element in Left Set Implies Element in Union

Informal description

For any element $x$ of type $\alpha$ and any sets $a, b$ of type $\alpha$, if $x$ is an element of $a$, then $x$ is an element of the union $a \cup b$.

Set.mem_union_right theorem

{x : α} {b : Set α} (a : Set α) : x ∈ b → x ∈ a ∪ b

Full source

theorem mem_union_right {x : α} {b : Set α} (a : Set α) : x ∈ b → x ∈ a ∪ b :=
  Or.inr

Membership in Union from Right: $x \in b \to x \in a \cup b$

Informal description

For any element $x$ of type $\alpha$ and any sets $a, b$ of type $\alpha$, if $x$ is an element of $b$, then $x$ is an element of the union $a \cup b$.

Set.mem_or_mem_of_mem_union theorem

{x : α} {a b : Set α} (H : x ∈ a ∪ b) : x ∈ a ∨ x ∈ b

Full source

theorem mem_or_mem_of_mem_union {x : α} {a b : Set α} (H : x ∈ a ∪ b) : x ∈ ax ∈ a ∨ x ∈ b :=
  H

Element in Union Implies Element in One of the Sets

Informal description

For any element $x$ of type $\alpha$ and any sets $a, b \subseteq \alpha$, if $x$ belongs to the union $a \cup b$, then $x$ belongs to $a$ or $x$ belongs to $b$.

Set.MemUnion.elim theorem

{x : α} {a b : Set α} {P : Prop} (H₁ : x ∈ a ∪ b) (H₂ : x ∈ a → P) (H₃ : x ∈ b → P) : P

Full source

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

Elimination Rule for Union Membership

Informal description

For any element $x$ of type $\alpha$ and sets $a, b \subseteq \alpha$, if $x$ belongs to the union $a \cup b$, then for any proposition $P$, if $x \in a$ implies $P$ and $x \in b$ implies $P$, then $P$ holds.

Set.mem_union theorem

(x : α) (a b : Set α) : x ∈ a ∪ b ↔ x ∈ a ∨ x ∈ b

Full source

@[simp]
theorem mem_union (x : α) (a b : Set α) : x ∈ a ∪ bx ∈ a ∪ b ↔ x ∈ a ∨ x ∈ b :=
  Iff.rfl

Characterization of Set Union Membership: $x \in a \cup b \leftrightarrow x \in a \lor x \in b$

Informal description

For any element $x$ of type $\alpha$ and any sets $a, b \subseteq \alpha$, the element $x$ belongs to the union $a \cup b$ if and only if $x$ belongs to $a$ or $x$ belongs to $b$.

Set.union_self theorem

(a : Set α) : a ∪ a = a

Full source

@[simp]
theorem union_self (a : Set α) : a ∪ a = a :=
  ext fun _ => or_self_iff

Idempotence of Set Union: $a \cup a = a$

Informal description

For any set $a$ over a type $\alpha$, the union of $a$ with itself equals $a$, i.e., $a \cup a = a$.

Set.union_empty theorem

(a : Set α) : a ∪ ∅ = a

Full source

@[simp]
theorem union_empty (a : Set α) : a ∪ ∅ = a :=
  ext fun _ => iff_of_eq (or_false _)

Union with Empty Set: $a \cup \emptyset = a$

Informal description

For any set $a$ over a type $\alpha$, the union of $a$ with the empty set equals $a$, i.e., $a \cup \emptyset = a$.

Set.empty_union theorem

(a : Set α) : ∅ ∪ a = a

Full source

@[simp]
theorem empty_union (a : Set α) : ∅∅ ∪ a = a :=
  ext fun _ => iff_of_eq (false_or _)

Empty Set Union Identity: $\emptyset \cup a = a$

Informal description

For any set $a$ over a type $\alpha$, the union of the empty set with $a$ equals $a$, i.e., $\emptyset \cup a = a$.

Set.union_comm theorem

(a b : Set α) : a ∪ b = b ∪ a

Full source

theorem union_comm (a b : Set α) : a ∪ b = b ∪ a :=
  ext fun _ => or_comm

Commutativity of Set Union: $a \cup b = b \cup a$

Informal description

For any two sets $a$ and $b$ over a type $\alpha$, the union $a \cup b$ is equal to $b \cup a$.

Set.union_assoc theorem

(a b c : Set α) : a ∪ b ∪ c = a ∪ (b ∪ c)

Full source

theorem union_assoc (a b c : Set α) : a ∪ ba ∪ b ∪ c = a ∪ (b ∪ c) :=
  ext fun _ => or_assoc

Associativity of Set Union: $(a \cup b) \cup c = a \cup (b \cup c)$

Informal description

For any sets $a$, $b$, and $c$ over a type $\alpha$, the union operation is associative, i.e., $(a \cup b) \cup c = a \cup (b \cup c)$.

Set.union_isAssoc instance

: Std.Associative (α := Set α) (· ∪ ·)

Full source

instance union_isAssoc : Std.Associative (α := Set α) (· ∪ ·) :=
  ⟨union_assoc⟩

Associativity of Set Union

Informal description

The union operation $\cup$ on sets is associative. That is, for any type $\alpha$ and sets $s_1, s_2, s_3$ of type $\alpha$, the operation satisfies $(s_1 \cup s_2) \cup s_3 = s_1 \cup (s_2 \cup s_3)$.

Set.union_isComm instance

: Std.Commutative (α := Set α) (· ∪ ·)

Full source

instance union_isComm : Std.Commutative (α := Set α) (· ∪ ·) :=
  ⟨union_comm⟩

Commutativity of Set Union

Informal description

The union operation $\cup$ on sets is commutative. That is, for any type $\alpha$ and sets $s_1, s_2$ of type $\alpha$, the operation satisfies $s_1 \cup s_2 = s_2 \cup s_1$.

Set.union_left_comm theorem

(s₁ s₂ s₃ : Set α) : s₁ ∪ (s₂ ∪ s₃) = s₂ ∪ (s₁ ∪ s₃)

Full source

theorem union_left_comm (s₁ s₂ s₃ : Set α) : s₁ ∪ (s₂ ∪ s₃) = s₂ ∪ (s₁ ∪ s₃) :=
  ext fun _ => or_left_comm

Left Commutativity of Set Union

Informal description

For any sets $s₁, s₂, s₃$ over a type $\alpha$, the union operation satisfies the left commutativity property: $s₁ ∪ (s₂ ∪ s₃) = s₂ ∪ (s₁ ∪ s₃)$.

Set.union_right_comm theorem

(s₁ s₂ s₃ : Set α) : s₁ ∪ s₂ ∪ s₃ = s₁ ∪ s₃ ∪ s₂

Full source

theorem union_right_comm (s₁ s₂ s₃ : Set α) : s₁ ∪ s₂s₁ ∪ s₂ ∪ s₃ = s₁ ∪ s₃s₁ ∪ s₃ ∪ s₂ :=
  ext fun _ => or_right_comm

Right Commutativity of Set Union

Informal description

For any sets $s₁, s₂, s₃$ over a type $\alpha$, the union operation satisfies the right commutativity property: $$s₁ ∪ s₂ ∪ s₃ = s₁ ∪ s₃ ∪ s₂$$

Set.union_eq_left theorem

{s t : Set α} : s ∪ t = s ↔ t ⊆ s

Full source

@[simp]
theorem union_eq_left {s t : Set α} : s ∪ ts ∪ t = s ↔ t ⊆ s :=
  sup_eq_left

Union Equals Left Set iff Right Subset

Informal description

For any sets $s$ and $t$ over a type $\alpha$, the union $s \cup t$ equals $s$ if and only if $t$ is a subset of $s$.

Set.union_eq_right theorem

{s t : Set α} : s ∪ t = t ↔ s ⊆ t

Full source

@[simp]
theorem union_eq_right {s t : Set α} : s ∪ ts ∪ t = t ↔ s ⊆ t :=
  sup_eq_right

Union Equals Right Operand iff Left Operand is Subset

Informal description

For any sets $s$ and $t$ over a type $\alpha$, the union $s \cup t$ equals $t$ if and only if $s$ is a subset of $t$.

Set.union_eq_self_of_subset_left theorem

{s t : Set α} (h : s ⊆ t) : s ∪ t = t

Full source

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

Union with Superset Equals Superset

Informal description

For any sets $s$ and $t$ over a type $\alpha$, if $s$ is a subset of $t$, then the union $s \cup t$ equals $t$.

Set.union_eq_self_of_subset_right theorem

{s t : Set α} (h : t ⊆ s) : s ∪ t = s

Full source

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

Union with Subset Equals Original Set (Right Version)

Informal description

For any sets $s$ and $t$ over a type $\alpha$, if $t$ is a subset of $s$, then the union $s \cup t$ equals $s$.

Set.subset_union_left theorem

{s t : Set α} : s ⊆ s ∪ t

Full source

@[simp]
theorem subset_union_left {s t : Set α} : s ⊆ s ∪ t := fun _ => Or.inl

Left Set is Subset of Union

Informal description

For any sets $s$ and $t$ over a type $\alpha$, the set $s$ is a subset of the union $s \cup t$.

Set.subset_union_right theorem

{s t : Set α} : t ⊆ s ∪ t

Full source

@[simp]
theorem subset_union_right {s t : Set α} : t ⊆ s ∪ t := fun _ => Or.inr

Right Set is Subset of Union

Informal description

For any two sets $s$ and $t$ over a type $\alpha$, the set $t$ is a subset of the union $s \cup t$.

Set.union_subset theorem

{s t r : Set α} (sr : s ⊆ r) (tr : t ⊆ r) : s ∪ t ⊆ r

Full source

theorem union_subset {s t r : Set α} (sr : s ⊆ r) (tr : t ⊆ r) : s ∪ ts ∪ t ⊆ r := fun _ =>
  Or.rec (@sr _) (@tr _)

Union Subset Property

Informal description

For any sets $s$, $t$, and $r$ in a type $\alpha$, if $s$ is a subset of $r$ and $t$ is a subset of $r$, then the union $s \cup t$ is also a subset of $r$.

Set.union_subset_iff theorem

{s t u : Set α} : s ∪ t ⊆ u ↔ s ⊆ u ∧ t ⊆ u

Full source

@[simp]
theorem union_subset_iff {s t u : Set α} : s ∪ ts ∪ t ⊆ us ∪ t ⊆ u ↔ s ⊆ u ∧ t ⊆ u :=
  (forall_congr' fun _ => or_imp).trans forall_and

Union Subset Criterion: $s \cup t \subseteq u \leftrightarrow s \subseteq u \land t \subseteq u$

Informal description

For any sets $s, t, u$ of type $\alpha$, the union $s \cup t$ is a subset of $u$ if and only if both $s$ is a subset of $u$ and $t$ is a subset of $u$.

Set.union_subset_union theorem

{s₁ s₂ t₁ t₂ : Set α} (h₁ : s₁ ⊆ s₂) (h₂ : t₁ ⊆ t₂) : s₁ ∪ t₁ ⊆ s₂ ∪ t₂

Full source

@[gcongr]
theorem union_subset_union {s₁ s₂ t₁ t₂ : Set α} (h₁ : s₁ ⊆ s₂) (h₂ : t₁ ⊆ t₂) :
    s₁ ∪ t₁s₁ ∪ t₁ ⊆ s₂ ∪ t₂ := fun _ => Or.imp (@h₁ _) (@h₂ _)

Monotonicity of Union with Respect to Subset

Informal description

For any sets $s₁, s₂, t₁, t₂$ of type $\alpha$, if $s₁ \subseteq s₂$ and $t₁ \subseteq t₂$, then $s₁ \cup t₁ \subseteq s₂ \cup t₂$.

Set.union_subset_union_left theorem

{s₁ s₂ : Set α} (t) (h : s₁ ⊆ s₂) : s₁ ∪ t ⊆ s₂ ∪ t

Full source

@[gcongr]
theorem union_subset_union_left {s₁ s₂ : Set α} (t) (h : s₁ ⊆ s₂) : s₁ ∪ ts₁ ∪ t ⊆ s₂ ∪ t :=
  union_subset_union h Subset.rfl

Left Union Monotonicity with Respect to Subset

Informal description

For any sets $s₁, s₂, t$ of type $\alpha$, if $s₁ \subseteq s₂$, then $s₁ \cup t \subseteq s₂ \cup t$.

Set.union_subset_union_right theorem

(s) {t₁ t₂ : Set α} (h : t₁ ⊆ t₂) : s ∪ t₁ ⊆ s ∪ t₂

Full source

@[gcongr]
theorem union_subset_union_right (s) {t₁ t₂ : Set α} (h : t₁ ⊆ t₂) : s ∪ t₁s ∪ t₁ ⊆ s ∪ t₂ :=
  union_subset_union Subset.rfl h

Right Union Monotonicity with Respect to Subset

Informal description

For any set $s$ of elements of type $\alpha$ and any sets $t₁, t₂$ of elements of type $\alpha$, if $t₁ \subseteq t₂$, then $s \cup t₁ \subseteq s \cup t₂$.

Set.subset_union_of_subset_left theorem

{s t : Set α} (h : s ⊆ t) (u : Set α) : s ⊆ t ∪ u

Full source

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

Subset Preservation under Union Extension

Informal description

For any sets $s, t, u$ over a type $\alpha$, if $s$ is a subset of $t$, then $s$ is also a subset of the union $t \cup u$.

Set.subset_union_of_subset_right theorem

{s u : Set α} (h : s ⊆ u) (t : Set α) : s ⊆ t ∪ u

Full source

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

Subset Preservation under Right Union Extension

Informal description

For any sets $s$ and $u$ over a type $\alpha$, if $s$ is a subset of $u$, then for any set $t$ over $\alpha$, $s$ is also a subset of the union $t \cup u$.

Set.union_congr_left theorem

(ht : t ⊆ s ∪ u) (hu : u ⊆ s ∪ t) : s ∪ t = s ∪ u

Full source

theorem union_congr_left (ht : t ⊆ s ∪ u) (hu : u ⊆ s ∪ t) : s ∪ t = s ∪ u :=
  sup_congr_left ht hu

Union Equality under Absorption Conditions

Informal description

For any sets $s, t, u$ in a type $\alpha$, if $t$ is a subset of $s \cup u$ and $u$ is a subset of $s \cup t$, then the unions $s \cup t$ and $s \cup u$ are equal, i.e., $s \cup t = s \cup u$.

Set.union_congr_right theorem

(hs : s ⊆ t ∪ u) (ht : t ⊆ s ∪ u) : s ∪ u = t ∪ u

Full source

theorem union_congr_right (hs : s ⊆ t ∪ u) (ht : t ⊆ s ∪ u) : s ∪ u = t ∪ u :=
  sup_congr_right hs ht

Union Equality under Mutual Subset Conditions

Informal description

For any sets $s$, $t$, and $u$ in a type $\alpha$, if $s$ is a subset of $t \cup u$ and $t$ is a subset of $s \cup u$, then the unions $s \cup u$ and $t \cup u$ are equal, i.e., $s \cup u = t \cup u$.

Set.union_eq_union_iff_left theorem

: s ∪ t = s ∪ u ↔ t ⊆ s ∪ u ∧ u ⊆ s ∪ t

Full source

theorem union_eq_union_iff_left : s ∪ ts ∪ t = s ∪ u ↔ t ⊆ s ∪ u ∧ u ⊆ s ∪ t :=
  sup_eq_sup_iff_left

Equality of Left Unions in Set Theory: $s \cup t = s \cup u \leftrightarrow t \subseteq s \cup u \land u \subseteq s \cup t$

Informal description

For any sets $s, t, u$ of elements of type $\alpha$, the equality $s \cup t = s \cup u$ holds if and only if $t$ is a subset of $s \cup u$ and $u$ is a subset of $s \cup t$.

Set.union_eq_union_iff_right theorem

: s ∪ u = t ∪ u ↔ s ⊆ t ∪ u ∧ t ⊆ s ∪ u

Full source

theorem union_eq_union_iff_right : s ∪ us ∪ u = t ∪ u ↔ s ⊆ t ∪ u ∧ t ⊆ s ∪ u :=
  sup_eq_sup_iff_right

Union Equality Criterion via Right Absorption Conditions

Informal description

For any sets $s$, $t$, and $u$ over a type $\alpha$, the equality $s \cup u = t \cup u$ holds if and only if $s$ is a subset of $t \cup u$ and $t$ is a subset of $s \cup u$.

Set.union_empty_iff theorem

{s t : Set α} : s ∪ t = ∅ ↔ s = ∅ ∧ t = ∅

Full source

@[simp]
theorem union_empty_iff {s t : Set α} : s ∪ ts ∪ t = ∅ ↔ s = ∅ ∧ t = ∅ := by
  simp only [← subset_empty_iff]
  exact union_subset_iff

Union is Empty iff Both Sets are Empty

Informal description

For any sets $s$ and $t$ of type $\alpha$, the union $s \cup t$ is equal to the empty set if and only if both $s$ and $t$ are equal to the empty set.

Set.union_univ theorem

(s : Set α) : s ∪ univ = univ

Full source

@[simp]
theorem union_univ (s : Set α) : s ∪ univ = univ := sup_top_eq _

Union with Universal Set Yields Universal Set

Informal description

For any set $s$ of elements of type $\alpha$, the union of $s$ with the universal set $\text{univ}$ equals $\text{univ}$. That is, $s \cup \text{univ} = \text{univ}$.

Set.univ_union theorem

(s : Set α) : univ ∪ s = univ

Full source

@[simp]
theorem univ_union (s : Set α) : univuniv ∪ s = univ := top_sup_eq _

Universal Set Absorbs Union

Informal description

For any set $s$ of elements of type $\alpha$, the union of the universal set (containing all elements of $\alpha$) with $s$ equals the universal set, i.e., $\text{univ} \cup s = \text{univ}$.

Set.ssubset_union_left_iff theorem

: s ⊂ s ∪ t ↔ ¬t ⊆ s

Full source

@[simp]
theorem ssubset_union_left_iff : s ⊂ s ∪ ts ⊂ s ∪ t ↔ ¬ t ⊆ s :=
  left_lt_sup

Strict subset relation with left union: $s \subset s \cup t \leftrightarrow t \not\subseteq s$

Informal description

For any sets $s$ and $t$ of elements of type $\alpha$, the strict inclusion $s \subset s \cup t$ holds if and only if $t$ is not a subset of $s$.

Set.ssubset_union_right_iff theorem

: t ⊂ s ∪ t ↔ ¬s ⊆ t

Full source

@[simp]
theorem ssubset_union_right_iff : t ⊂ s ∪ tt ⊂ s ∪ t ↔ ¬ s ⊆ t :=
  right_lt_sup

Strict Subset of Right Union: $t \subset s \cup t \leftrightarrow s \not\subseteq t$

Informal description

For any sets $s$ and $t$ of elements of type $\alpha$, the set $t$ is a strict subset of the union $s \cup t$ if and only if $s$ is not a subset of $t$, i.e., $t \subset s \cup t \leftrightarrow s \not\subseteq t$.

Set.inter_def theorem

{s₁ s₂ : Set α} : s₁ ∩ s₂ = {a | a ∈ s₁ ∧ a ∈ s₂}

Full source

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

Definition of Set Intersection via Comprehension

Informal description

For any two sets $s_1$ and $s_2$ in a type $\alpha$, their intersection $s_1 \cap s_2$ is equal to the set $\{a \in \alpha \mid a \in s_1 \text{ and } a \in s_2\}$.

Set.mem_inter_iff theorem

(x : α) (a b : Set α) : x ∈ a ∩ b ↔ x ∈ a ∧ x ∈ b

Full source

@[simp, mfld_simps]
theorem mem_inter_iff (x : α) (a b : Set α) : x ∈ a ∩ bx ∈ a ∩ b ↔ x ∈ a ∧ x ∈ b :=
  Iff.rfl

Membership in Set Intersection is Equivalent to Membership in Both Sets

Informal description

For any element $x$ of type $\alpha$ and any two sets $a, b \subseteq \alpha$, the element $x$ belongs to the intersection $a \cap b$ if and only if $x$ belongs to both $a$ and $b$. In other words, $x \in a \cap b \leftrightarrow x \in a \land x \in b$.

Set.mem_inter theorem

{x : α} {a b : Set α} (ha : x ∈ a) (hb : x ∈ b) : x ∈ a ∩ b

Full source

theorem mem_inter {x : α} {a b : Set α} (ha : x ∈ a) (hb : x ∈ b) : x ∈ a ∩ b :=
  ⟨ha, hb⟩

Membership in Intersection from Membership in Both Sets

Informal description

For any element $x$ of type $\alpha$ and any sets $a, b \subseteq \alpha$, if $x \in a$ and $x \in b$, then $x$ belongs to their intersection $a \cap b$.

Set.mem_of_mem_inter_left theorem

{x : α} {a b : Set α} (h : x ∈ a ∩ b) : x ∈ a

Full source

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

Element of Intersection is in Left Set

Informal description

For any element $x$ of type $\alpha$ and any sets $a, b \subseteq \alpha$, if $x$ belongs to the intersection $a \cap b$, then $x$ belongs to $a$.

Set.mem_of_mem_inter_right theorem

{x : α} {a b : Set α} (h : x ∈ a ∩ b) : x ∈ b

Full source

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

Element of Intersection is in Right Set

Informal description

For any element $x$ of type $\alpha$ and any sets $a, b \subseteq \alpha$, if $x$ belongs to the intersection $a \cap b$, then $x$ belongs to $b$.

Set.inter_self theorem

(a : Set α) : a ∩ a = a

Full source

@[simp]
theorem inter_self (a : Set α) : a ∩ a = a :=
  ext fun _ => and_self_iff

Idempotence of Set Intersection: $a \cap a = a$

Informal description

For any set $a$ over a type $\alpha$, the intersection of $a$ with itself is equal to $a$, i.e., $a \cap a = a$.

Set.inter_empty theorem

(a : Set α) : a ∩ ∅ = ∅

Full source

@[simp]
theorem inter_empty (a : Set α) : a ∩ ∅ = ∅ :=
  ext fun _ => iff_of_eq (and_false _)

Intersection with Empty Set Yields Empty Set

Informal description

For any set $a$ over a type $\alpha$, the intersection of $a$ with the empty set is the empty set, i.e., $a \cap \emptyset = \emptyset$.

Set.empty_inter theorem

(a : Set α) : ∅ ∩ a = ∅

Full source

@[simp]
theorem empty_inter (a : Set α) : ∅∅ ∩ a = ∅ :=
  ext fun _ => iff_of_eq (false_and _)

Intersection with Empty Set Yields Empty Set

Informal description

For any set $a$ over a type $\alpha$, the intersection of the empty set with $a$ is the empty set, i.e., $\emptyset \cap a = \emptyset$.

Set.inter_comm theorem

(a b : Set α) : a ∩ b = b ∩ a

Full source

theorem inter_comm (a b : Set α) : a ∩ b = b ∩ a :=
  ext fun _ => and_comm

Commutativity of Set Intersection: $a \cap b = b \cap a$

Informal description

For any two sets $a$ and $b$ over a type $\alpha$, the intersection $a \cap b$ is equal to $b \cap a$.

Set.inter_assoc theorem

(a b c : Set α) : a ∩ b ∩ c = a ∩ (b ∩ c)

Full source

theorem inter_assoc (a b c : Set α) : a ∩ ba ∩ b ∩ c = a ∩ (b ∩ c) :=
  ext fun _ => and_assoc

Associativity of Set Intersection: $(a \cap b) \cap c = a \cap (b \cap c)$

Informal description

For any sets $a$, $b$, and $c$ over a type $\alpha$, the intersection operation is associative, i.e., $(a \cap b) \cap c = a \cap (b \cap c)$.

Set.inter_isAssoc instance

: Std.Associative (α := Set α) (· ∩ ·)

Full source

instance inter_isAssoc : Std.Associative (α := Set α) (· ∩ ·) :=
  ⟨inter_assoc⟩

Associativity of Set Intersection

Informal description

The intersection operation $\cap$ on sets is associative.

Set.inter_isComm instance

: Std.Commutative (α := Set α) (· ∩ ·)

Full source

instance inter_isComm : Std.Commutative (α := Set α) (· ∩ ·) :=
  ⟨inter_comm⟩

Commutativity of Set Intersection

Informal description

The intersection operation $\cap$ on sets over any type $\alpha$ is commutative.

Set.inter_left_comm theorem

(s₁ s₂ s₃ : Set α) : s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃)

Full source

theorem inter_left_comm (s₁ s₂ s₃ : Set α) : s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃) :=
  ext fun _ => and_left_comm

Left Commutativity of Set Intersection: $s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃)$

Informal description

For any sets $s₁, s₂, s₃$ over a type $\alpha$, the intersection operation satisfies the left commutativity property: $$s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃)$$

Set.inter_right_comm theorem

(s₁ s₂ s₃ : Set α) : s₁ ∩ s₂ ∩ s₃ = s₁ ∩ s₃ ∩ s₂

Full source

theorem inter_right_comm (s₁ s₂ s₃ : Set α) : s₁ ∩ s₂s₁ ∩ s₂ ∩ s₃ = s₁ ∩ s₃s₁ ∩ s₃ ∩ s₂ :=
  ext fun _ => and_right_comm

Right Commutativity of Set Intersection: $s_1 \cap s_2 \cap s_3 = s_1 \cap s_3 \cap s_2$

Informal description

For any three sets $s_1, s_2, s_3$ over a type $\alpha$, the intersection $s_1 \cap s_2 \cap s_3$ is equal to $s_1 \cap s_3 \cap s_2$.

Set.inter_subset_left theorem

{s t : Set α} : s ∩ t ⊆ s

Full source

@[simp, mfld_simps]
theorem inter_subset_left {s t : Set α} : s ∩ ts ∩ t ⊆ s := fun _ => And.left

Intersection is Subset of Left Operand: $s \cap t \subseteq s$

Informal description

For any sets $s$ and $t$ over a type $\alpha$, the intersection $s \cap t$ is a subset of $s$.

Set.inter_subset_right theorem

{s t : Set α} : s ∩ t ⊆ t

Full source

@[simp]
theorem inter_subset_right {s t : Set α} : s ∩ ts ∩ t ⊆ t := fun _ => And.right

Intersection is a Subset of the Second Set: $s \cap t \subseteq t$

Informal description

For any two sets $s$ and $t$ over a type $\alpha$, the intersection $s \cap t$ is a subset of $t$.

Set.subset_inter theorem

{s t r : Set α} (rs : r ⊆ s) (rt : r ⊆ t) : r ⊆ s ∩ t

Full source

theorem subset_inter {s t r : Set α} (rs : r ⊆ s) (rt : r ⊆ t) : r ⊆ s ∩ t := fun _ h =>
  ⟨rs h, rt h⟩

Subset of Intersection from Subsets of Components

Informal description

For any sets $r, s, t$ in a type $\alpha$, if $r$ is a subset of $s$ and $r$ is a subset of $t$, then $r$ is a subset of the intersection $s \cap t$.

Set.subset_inter_iff theorem

{s t r : Set α} : r ⊆ s ∩ t ↔ r ⊆ s ∧ r ⊆ t

Full source

@[simp]
theorem subset_inter_iff {s t r : Set α} : r ⊆ s ∩ tr ⊆ s ∩ t ↔ r ⊆ s ∧ r ⊆ t :=
  (forall_congr' fun _ => imp_and).trans forall_and

Subset of Intersection Equivales to Subset of Both Sets

Informal description

For any sets $r, s, t$ over a type $\alpha$, the subset relation $r \subseteq s \cap t$ holds if and only if both $r \subseteq s$ and $r \subseteq t$ hold.

Set.inter_eq_left theorem

: s ∩ t = s ↔ s ⊆ t

Full source

@[simp] lemma inter_eq_left : s ∩ ts ∩ t = s ↔ s ⊆ t := inf_eq_left

Intersection Equals Left Set if and only if Left is Subset of Right

Informal description

For any sets $s$ and $t$ over a type $\alpha$, the intersection $s \cap t$ equals $s$ if and only if $s$ is a subset of $t$.

Set.inter_eq_right theorem

: s ∩ t = t ↔ t ⊆ s

Full source

@[simp] lemma inter_eq_right : s ∩ ts ∩ t = t ↔ t ⊆ s := inf_eq_right

Intersection Equals Right Set if and only if Right is Subset of Left

Informal description

For any sets $s$ and $t$ over a type $\alpha$, the intersection $s \cap t$ equals $t$ if and only if $t$ is a subset of $s$.

Set.left_eq_inter theorem

: s = s ∩ t ↔ s ⊆ t

Full source

@[simp] lemma left_eq_inter : s = s ∩ t ↔ s ⊆ t := left_eq_inf

Set Equality via Intersection: $s = s \cap t \leftrightarrow s \subseteq t$

Informal description

For any sets $s$ and $t$ of type $\alpha$, the equality $s = s \cap t$ holds if and only if $s$ is a subset of $t$.

Set.right_eq_inter theorem

: t = s ∩ t ↔ t ⊆ s

Full source

@[simp] lemma right_eq_inter : t = s ∩ t ↔ t ⊆ s := right_eq_inf

Right Set Equals Intersection if and only if Right is Subset of Left

Informal description

For any sets $s$ and $t$ over a type $\alpha$, the equality $t = s \cap t$ holds if and only if $t$ is a subset of $s$, i.e., $t \subseteq s$.

Set.inter_eq_self_of_subset_left theorem

{s t : Set α} : s ⊆ t → s ∩ t = s

Full source

theorem inter_eq_self_of_subset_left {s t : Set α} : s ⊆ t → s ∩ t = s :=
  inter_eq_left.mpr

Intersection with Superset Equals Left Set

Informal description

For any sets $s$ and $t$ over a type $\alpha$, if $s$ is a subset of $t$, then the intersection $s \cap t$ equals $s$.

Set.inter_eq_self_of_subset_right theorem

{s t : Set α} : t ⊆ s → s ∩ t = t

Full source

theorem inter_eq_self_of_subset_right {s t : Set α} : t ⊆ s → s ∩ t = t :=
  inter_eq_right.mpr

Intersection Equals Subset When Right is Subset of Left

Informal description

For any sets $s$ and $t$ over a type $\alpha$, if $t$ is a subset of $s$, then the intersection $s \cap t$ equals $t$.

Set.inter_congr_left theorem

(ht : s ∩ u ⊆ t) (hu : s ∩ t ⊆ u) : s ∩ t = s ∩ u

Full source

theorem inter_congr_left (ht : s ∩ us ∩ u ⊆ t) (hu : s ∩ ts ∩ t ⊆ u) : s ∩ t = s ∩ u :=
  inf_congr_left ht hu

Intersection Congruence under Absorption Conditions

Informal description

For any sets $s$, $t$, and $u$ in a type $\alpha$, if $s \cap u \subseteq t$ and $s \cap t \subseteq u$, then $s \cap t = s \cap u$.

Set.inter_congr_right theorem

(hs : t ∩ u ⊆ s) (ht : s ∩ u ⊆ t) : s ∩ u = t ∩ u

Full source

theorem inter_congr_right (hs : t ∩ ut ∩ u ⊆ s) (ht : s ∩ us ∩ u ⊆ t) : s ∩ u = t ∩ u :=
  inf_congr_right hs ht

Intersection Equality under Subset Conditions: $s \cap u = t \cap u$

Informal description

For any sets $s$, $t$, and $u$ in a type $\alpha$, if the intersection $t \cap u$ is a subset of $s$ and the intersection $s \cap u$ is a subset of $t$, then the intersections $s \cap u$ and $t \cap u$ are equal, i.e., $s \cap u = t \cap u$.

Set.inter_eq_inter_iff_left theorem

: s ∩ t = s ∩ u ↔ s ∩ u ⊆ t ∧ s ∩ t ⊆ u

Full source

theorem inter_eq_inter_iff_left : s ∩ ts ∩ t = s ∩ u ↔ s ∩ u ⊆ t ∧ s ∩ t ⊆ u :=
  inf_eq_inf_iff_left

Intersection Equality under Subset Conditions: $s \cap t = s \cap u \leftrightarrow (s \cap u \subseteq t \land s \cap t \subseteq u)$

Informal description

For any sets $s$, $t$, and $u$ in a type $\alpha$, the equality $s \cap t = s \cap u$ holds if and only if $s \cap u$ is a subset of $t$ and $s \cap t$ is a subset of $u$.

Set.inter_eq_inter_iff_right theorem

: s ∩ u = t ∩ u ↔ t ∩ u ⊆ s ∧ s ∩ u ⊆ t

Full source

theorem inter_eq_inter_iff_right : s ∩ us ∩ u = t ∩ u ↔ t ∩ u ⊆ s ∧ s ∩ u ⊆ t :=
  inf_eq_inf_iff_right

Intersection Equality Criterion via Subset Conditions: $s \cap u = t \cap u$

Informal description

For any sets $s$, $t$, and $u$ of type $\alpha$, the equality $s \cap u = t \cap u$ holds if and only if $t \cap u$ is a subset of $s$ and $s \cap u$ is a subset of $t$.

Set.inter_univ theorem

(a : Set α) : a ∩ univ = a

Full source

@[simp, mfld_simps]
theorem inter_univ (a : Set α) : a ∩ univ = a := inf_top_eq _

Intersection with Universal Set: $a \cap \text{univ} = a$

Informal description

For any set $a$ of type $\alpha$, the intersection of $a$ with the universal set equals $a$, i.e., $a \cap \text{univ} = a$.

Set.univ_inter theorem

(a : Set α) : univ ∩ a = a

Full source

@[simp, mfld_simps]
theorem univ_inter (a : Set α) : univuniv ∩ a = a := top_inf_eq _

Intersection with Universal Set: $\text{univ} \cap a = a$

Informal description

For any set $a$ of type $\alpha$, the intersection of the universal set with $a$ equals $a$, i.e., $\text{univ} \cap a = a$.

Set.inter_subset_inter theorem

{s₁ s₂ t₁ t₂ : Set α} (h₁ : s₁ ⊆ t₁) (h₂ : s₂ ⊆ t₂) : s₁ ∩ s₂ ⊆ t₁ ∩ t₂

Full source

@[gcongr]
theorem inter_subset_inter {s₁ s₂ t₁ t₂ : Set α} (h₁ : s₁ ⊆ t₁) (h₂ : s₂ ⊆ t₂) :
    s₁ ∩ s₂s₁ ∩ s₂ ⊆ t₁ ∩ t₂ := fun _ => And.imp (@h₁ _) (@h₂ _)

Intersection Preserves Subset Relation

Informal description

For any sets $s₁, s₂, t₁, t₂$ of type $\alpha$, if $s₁ \subseteq t₁$ and $s₂ \subseteq t₂$, then the intersection $s₁ \cap s₂$ is a subset of $t₁ \cap t₂$.

Set.inter_subset_inter_left theorem

{s t : Set α} (u : Set α) (H : s ⊆ t) : s ∩ u ⊆ t ∩ u

Full source

@[gcongr]
theorem inter_subset_inter_left {s t : Set α} (u : Set α) (H : s ⊆ t) : s ∩ us ∩ u ⊆ t ∩ u :=
  inter_subset_inter H Subset.rfl

Left Intersection Preserves Subset Relation

Informal description

For any sets $s, t, u$ of type $\alpha$, if $s \subseteq t$, then the intersection $s \cap u$ is a subset of $t \cap u$.

Set.inter_subset_inter_right theorem

{s t : Set α} (u : Set α) (H : s ⊆ t) : u ∩ s ⊆ u ∩ t

Full source

@[gcongr]
theorem inter_subset_inter_right {s t : Set α} (u : Set α) (H : s ⊆ t) : u ∩ su ∩ s ⊆ u ∩ t :=
  inter_subset_inter Subset.rfl H

Intersection Preserves Subset Relation (Right Variant)

Informal description

For any sets $s, t, u$ of elements of type $\alpha$, if $s$ is a subset of $t$, then the intersection $u \cap s$ is a subset of $u \cap t$.

Set.union_inter_cancel_left theorem

{s t : Set α} : (s ∪ t) ∩ s = s

Full source

theorem union_inter_cancel_left {s t : Set α} : (s ∪ t) ∩ s = s :=
  inter_eq_self_of_subset_right subset_union_left

Absorption Law for Union and Intersection (Left Variant)

Informal description

For any sets $s$ and $t$ of elements of type $\alpha$, the intersection of the union $s \cup t$ with $s$ equals $s$, i.e., $(s \cup t) \cap s = s$.

Set.union_inter_cancel_right theorem

{s t : Set α} : (s ∪ t) ∩ t = t

Full source

theorem union_inter_cancel_right {s t : Set α} : (s ∪ t) ∩ t = t :=
  inter_eq_self_of_subset_right subset_union_right

Absorption Law for Union and Intersection (Right Variant)

Informal description

For any sets $s$ and $t$ of elements of type $\alpha$, the intersection of the union $s \cup t$ with $t$ equals $t$, i.e., $(s \cup t) \cap t = t$.

Set.inter_setOf_eq_sep theorem

(s : Set α) (p : α → Prop) : s ∩ {a | p a} = {a ∈ s | p a}

Full source

theorem inter_setOf_eq_sep (s : Set α) (p : α → Prop) : s ∩ {a | p a} = {a ∈ s | p a} :=
  rfl

Intersection with Set Comprehension Equals Filtered Set

Informal description

For any set $s$ in type $\alpha$ and any predicate $p$ on $\alpha$, the intersection of $s$ with the set $\{a \mid p a\}$ is equal to the set $\{a \in s \mid p a\}$ of elements in $s$ that satisfy $p$.

Set.setOf_inter_eq_sep theorem

(p : α → Prop) (s : Set α) : {a | p a} ∩ s = {a ∈ s | p a}

Full source

theorem setOf_inter_eq_sep (p : α → Prop) (s : Set α) : {a | p a}{a | p a} ∩ s = {a ∈ s | p a} :=
  inter_comm _ _

Intersection of Set Comprehension with a Set Equals Filtered Set

Informal description

For any predicate $p$ on a type $\alpha$ and any set $s$ in $\alpha$, the intersection of the set $\{a \mid p a\}$ with $s$ is equal to the set $\{a \in s \mid p a\}$ of elements in $s$ that satisfy $p$.

Set.inter_ssubset_right_iff theorem

: s ∩ t ⊂ t ↔ ¬t ⊆ s

Full source

@[simp]
theorem inter_ssubset_right_iff : s ∩ ts ∩ t ⊂ ts ∩ t ⊂ t ↔ ¬ t ⊆ s :=
  inf_lt_right

Strict Subset Property of Intersection: $s \cap t \subset t \leftrightarrow t \nsubseteq s$

Informal description

For any sets $s$ and $t$ in a type $\alpha$, the intersection $s \cap t$ is a strict subset of $t$ if and only if $t$ is not a subset of $s$.

Set.inter_ssubset_left_iff theorem

: s ∩ t ⊂ s ↔ ¬s ⊆ t

Full source

@[simp]
theorem inter_ssubset_left_iff : s ∩ ts ∩ t ⊂ ss ∩ t ⊂ s ↔ ¬ s ⊆ t :=
  inf_lt_left

Strict Subset Property of Intersection: $s \cap t \subset s \leftrightarrow s \nsubseteq t$

Informal description

For any sets $s$ and $t$ in a type $\alpha$, the intersection $s \cap t$ is a strict subset of $s$ if and only if $s$ is not a subset of $t$.

Set.inter_union_distrib_left theorem

(s t u : Set α) : s ∩ (t ∪ u) = s ∩ t ∪ s ∩ u

Full source

theorem inter_union_distrib_left (s t u : Set α) : s ∩ (t ∪ u) = s ∩ ts ∩ t ∪ s ∩ u :=
  inf_sup_left _ _ _

Left Distributivity of Intersection over Union in Sets: $s \cap (t \cup u) = (s \cap t) \cup (s \cap u)$

Informal description

For any sets $s$, $t$, and $u$ over a type $\alpha$, the intersection of $s$ with the union of $t$ and $u$ equals the union of the intersections of $s$ with $t$ and $s$ with $u$: $$ s \cap (t \cup u) = (s \cap t) \cup (s \cap u). $$

Set.union_inter_distrib_right theorem

(s t u : Set α) : (s ∪ t) ∩ u = s ∩ u ∪ t ∩ u

Full source

theorem union_inter_distrib_right (s t u : Set α) : (s ∪ t) ∩ u = s ∩ us ∩ u ∪ t ∩ u :=
  inf_sup_right _ _ _

Right Distributivity of Intersection over Union in Sets: $(s \cup t) \cap u = (s \cap u) \cup (t \cap u)$

Informal description

For any sets $s, t, u$ over a type $\alpha$, the intersection of the union $s \cup t$ with $u$ equals the union of the intersections $s \cap u$ and $t \cap u$: $$ (s \cup t) \cap u = (s \cap u) \cup (t \cap u). $$

Set.union_inter_distrib_left theorem

(s t u : Set α) : s ∪ t ∩ u = (s ∪ t) ∩ (s ∪ u)

Full source

theorem union_inter_distrib_left (s t u : Set α) : s ∪ t ∩ u = (s ∪ t) ∩ (s ∪ u) :=
  sup_inf_left _ _ _

Left Distributivity of Union over Intersection in Sets: $s \cup (t \cap u) = (s \cup t) \cap (s \cup u)$

Informal description

For any sets $s, t, u$ over a type $\alpha$, the following equality holds: $$ s \cup (t \cap u) = (s \cup t) \cap (s \cup u). $$

Set.inter_union_distrib_right theorem

(s t u : Set α) : s ∩ t ∪ u = (s ∪ u) ∩ (t ∪ u)

Full source

theorem inter_union_distrib_right (s t u : Set α) : s ∩ ts ∩ t ∪ u = (s ∪ u) ∩ (t ∪ u) :=
  sup_inf_right _ _ _

Right Distributivity of Union over Intersection in Sets: $(s \cap t) \cup u = (s \cup u) \cap (t \cup u)$

Informal description

For any sets $s, t, u$ over a type $\alpha$, the following equality holds: $$ (s \cap t) \cup u = (s \cup u) \cap (t \cup u). $$

Set.union_union_distrib_left theorem

(s t u : Set α) : s ∪ (t ∪ u) = s ∪ t ∪ (s ∪ u)

Full source

theorem union_union_distrib_left (s t u : Set α) : s ∪ (t ∪ u) = s ∪ ts ∪ t ∪ (s ∪ u) :=
  sup_sup_distrib_left _ _ _

Left Distributivity of Union over Union in Sets

Informal description

For any sets $s, t, u$ over a type $\alpha$, the union operation satisfies the left distributivity property: $$s \cup (t \cup u) = (s \cup t) \cup (s \cup u)$$

Set.union_union_distrib_right theorem

(s t u : Set α) : s ∪ t ∪ u = s ∪ u ∪ (t ∪ u)

Full source

theorem union_union_distrib_right (s t u : Set α) : s ∪ ts ∪ t ∪ u = s ∪ us ∪ u ∪ (t ∪ u) :=
  sup_sup_distrib_right _ _ _

Right-Distributivity of Union Operation on Sets

Informal description

For any sets $s, t, u$ over a type $\alpha$, the union operation satisfies the following right-distributivity property: $$s \cup t \cup u = s \cup u \cup (t \cup u)$$

Set.inter_inter_distrib_left theorem

(s t u : Set α) : s ∩ (t ∩ u) = s ∩ t ∩ (s ∩ u)

Full source

theorem inter_inter_distrib_left (s t u : Set α) : s ∩ (t ∩ u) = s ∩ ts ∩ t ∩ (s ∩ u) :=
  inf_inf_distrib_left _ _ _

Left Distributivity of Intersection over Intersection in Sets

Informal description

For any sets $s, t, u$ over a type $\alpha$, the intersection operation satisfies the left distributivity property: $$s \cap (t \cap u) = (s \cap t) \cap (s \cap u)$$

Set.inter_inter_distrib_right theorem

(s t u : Set α) : s ∩ t ∩ u = s ∩ u ∩ (t ∩ u)

Full source

theorem inter_inter_distrib_right (s t u : Set α) : s ∩ ts ∩ t ∩ u = s ∩ us ∩ u ∩ (t ∩ u) :=
  inf_inf_distrib_right _ _ _

Right-Distributivity of Set Intersection: $s \cap t \cap u = s \cap u \cap (t \cap u)$

Informal description

For any sets $s, t, u$ over a type $\alpha$, the intersection operation satisfies the following right-distributivity property: $$ s \cap t \cap u = s \cap u \cap (t \cap u) $$

Set.union_union_union_comm theorem

(s t u v : Set α) : s ∪ t ∪ (u ∪ v) = s ∪ u ∪ (t ∪ v)

Full source

theorem union_union_union_comm (s t u v : Set α) : s ∪ ts ∪ t ∪ (u ∪ v) = s ∪ us ∪ u ∪ (t ∪ v) :=
  sup_sup_sup_comm _ _ _ _

Commutativity of Quadruple Union Operation: $s \cup t \cup (u \cup v) = s \cup u \cup (t \cup v)$

Informal description

For any sets $s, t, u, v$ in a type $\alpha$, the following equality holds: $$s \cup t \cup (u \cup v) = s \cup u \cup (t \cup v)$$

Set.inter_inter_inter_comm theorem

(s t u v : Set α) : s ∩ t ∩ (u ∩ v) = s ∩ u ∩ (t ∩ v)

Full source

theorem inter_inter_inter_comm (s t u v : Set α) : s ∩ ts ∩ t ∩ (u ∩ v) = s ∩ us ∩ u ∩ (t ∩ v) :=
  inf_inf_inf_comm _ _ _ _

Commutativity of Quadruple Set Intersection: $s \cap t \cap (u \cap v) = s \cap u \cap (t \cap v)$

Informal description

For any sets $s, t, u, v$ over a type $\alpha$, the following equality holds: $$ s \cap t \cap (u \cap v) = s \cap u \cap (t \cap v) $$

Set.mem_sep theorem

(xs : x ∈ s) (px : p x) : x ∈ {x ∈ s | p x}

Full source

theorem mem_sep (xs : x ∈ s) (px : p x) : x ∈ { x ∈ s | p x } :=
  ⟨xs, px⟩

Membership in Filtered Set

Informal description

For any element $x$ and set $s$, if $x \in s$ and $p(x)$ holds, then $x$ belongs to the subset $\{x \in s \mid p(x)\}$.

Set.sep_mem_eq theorem

: {x ∈ s | x ∈ t} = s ∩ t

Full source

@[simp]
theorem sep_mem_eq : { x ∈ s | x ∈ t } = s ∩ t :=
  rfl

Separation of Membership Equals Intersection

Informal description

For any sets $s$ and $t$ of elements of type $\alpha$, the set $\{x \in s \mid x \in t\}$ is equal to the intersection $s \cap t$.

Set.mem_sep_iff theorem

: x ∈ {x ∈ s | p x} ↔ x ∈ s ∧ p x

Full source

@[simp]
theorem mem_sep_iff : x ∈ { x ∈ s | p x }x ∈ { x ∈ s | p x } ↔ x ∈ s ∧ p x :=
  Iff.rfl

Membership in Separated Set Characterization

Informal description

For any element $x$ and sets $s$, the statement $x \in \{x \in s \mid p x\}$ holds if and only if $x \in s$ and $p x$ holds.

Set.sep_ext_iff theorem

: {x ∈ s | p x} = {x ∈ s | q x} ↔ ∀ x ∈ s, p x ↔ q x

Full source

theorem sep_ext_iff : { x ∈ s | p x }{ x ∈ s | p x } = { x ∈ s | q x } ↔ ∀ x ∈ s, p x ↔ q x := by
  simp_rw [Set.ext_iff, mem_sep_iff, and_congr_right_iff]

Characterization of Set Equality via Predicate Equivalence

Informal description

For any set $s$ and predicates $p, q$ on elements of $s$, the sets $\{x \in s \mid p x\}$ and $\{x \in s \mid q x\}$ are equal if and only if for every $x \in s$, $p x$ holds if and only if $q x$ holds.

Set.sep_eq_of_subset theorem

(h : s ⊆ t) : {x ∈ t | x ∈ s} = s

Full source

theorem sep_eq_of_subset (h : s ⊆ t) : { x ∈ t | x ∈ s } = s :=
  inter_eq_self_of_subset_right h

Separation Set Equals Subset When Subset Condition Holds

Informal description

For any sets $s$ and $t$ of elements of type $\alpha$, if $s$ is a subset of $t$, then the set $\{x \in t \mid x \in s\}$ is equal to $s$.

Set.sep_subset theorem

(s : Set α) (p : α → Prop) : {x ∈ s | p x} ⊆ s

Full source

@[simp]
theorem sep_subset (s : Set α) (p : α → Prop) : { x ∈ s | p x }{ x ∈ s | p x } ⊆ s := fun _ => And.left

Separation Set is Subset of Original Set

Informal description

For any set $s$ of elements of type $\alpha$ and any predicate $p$ on $\alpha$, the subset $\{x \in s \mid p x\}$ is contained in $s$.

Set.sep_eq_self_iff_mem_true theorem

: {x ∈ s | p x} = s ↔ ∀ x ∈ s, p x

Full source

@[simp]
theorem sep_eq_self_iff_mem_true : { x ∈ s | p x }{ x ∈ s | p x } = s ↔ ∀ x ∈ s, p x := by
  simp_rw [Set.ext_iff, mem_sep_iff, and_iff_left_iff_imp]

Characterization of Set Equality via Predicate Satisfaction

Informal description

For any set $s$ and predicate $p$ on elements of $s$, the subset $\{x \in s \mid p x\}$ equals $s$ if and only if every element $x$ in $s$ satisfies $p(x)$.

Set.sep_eq_empty_iff_mem_false theorem

: {x ∈ s | p x} = ∅ ↔ ∀ x ∈ s, ¬p x

Full source

@[simp]
theorem sep_eq_empty_iff_mem_false : { x ∈ s | p x }{ x ∈ s | p x } = ∅ ↔ ∀ x ∈ s, ¬p x := by
  simp_rw [Set.ext_iff, mem_sep_iff, mem_empty_iff_false, iff_false, not_and]

Empty Separation Set Characterization via Predicate Falsity

Informal description

For any set $s$ and predicate $p$ on elements of $s$, the subset $\{x \in s \mid p x\}$ is empty if and only if for every element $x$ in $s$, the predicate $p(x)$ does not hold.

Set.sep_true theorem

: {x ∈ s | True} = s

Full source

theorem sep_true : { x ∈ s | True } = s :=
  inter_univ s

Separation with Trivial Predicate Preserves Set

Informal description

For any set $s$, the subset $\{x \in s \mid \text{True}\}$ is equal to $s$ itself.

Set.sep_false theorem

: {x ∈ s | False} = ∅

Full source

theorem sep_false : { x ∈ s | False } = ∅ :=
  inter_empty s

Separation with False Predicate Yields Empty Set

Informal description

For any set $s$ over a type $\alpha$, the subset $\{x \in s \mid \text{False}\}$ is equal to the empty set $\emptyset$.

Set.sep_empty theorem

(p : α → Prop) : {x ∈ (∅ : Set α) | p x} = ∅

Full source

theorem sep_empty (p : α → Prop) : { x ∈ (∅ : Set α) | p x } = ∅ :=
  empty_inter {x | p x}

Separation over Empty Set Yields Empty Set

Informal description

For any predicate $p : \alpha \to \mathrm{Prop}$, the set $\{x \in \emptyset \mid p x\}$ is equal to the empty set $\emptyset$.

Set.sep_univ theorem

: {x ∈ (univ : Set α) | p x} = {x | p x}

Full source

theorem sep_univ : { x ∈ (univ : Set α) | p x } = { x | p x } :=
  univ_inter {x | p x}

Separation over Universal Set Equals Predicate Set

Informal description

For any predicate $p : \alpha \to \mathrm{Prop}$, the set $\{x \in \text{univ} \mid p x\}$ is equal to the set $\{x \mid p x\}$ of all elements satisfying $p$.

Set.sep_union theorem

: {x | (x ∈ s ∨ x ∈ t) ∧ p x} = {x ∈ s | p x} ∪ {x ∈ t | p x}

Full source

@[simp]
theorem sep_union : { x | (x ∈ s ∨ x ∈ t) ∧ p x } = { x ∈ s | p x }{ x ∈ s | p x } ∪ { x ∈ t | p x } :=
  union_inter_distrib_right { x | x ∈ s } { x | x ∈ t } p

Union of Filtered Sets: $\{x \mid (x \in s \lor x \in t) \land p x\} = \{x \in s \mid p x\} \cup \{x \in t \mid p x\}$

Informal description

For any sets $s, t$ over a type $\alpha$ and any predicate $p : \alpha \to \mathrm{Prop}$, the set of elements satisfying either membership in $s$ or $t$ and the predicate $p$ is equal to the union of the sets $\{x \in s \mid p x\}$ and $\{x \in t \mid p x\}$. In symbols: $$ \{x \mid (x \in s \lor x \in t) \land p x\} = \{x \in s \mid p x\} \cup \{x \in t \mid p x\} $$

Set.sep_inter theorem

: {x | (x ∈ s ∧ x ∈ t) ∧ p x} = {x ∈ s | p x} ∩ {x ∈ t | p x}

Full source

@[simp]
theorem sep_inter : { x | (x ∈ s ∧ x ∈ t) ∧ p x } = { x ∈ s | p x }{ x ∈ s | p x } ∩ { x ∈ t | p x } :=
  inter_inter_distrib_right s t {x | p x}

Separation over Intersection Equals Intersection of Separations

Informal description

For any sets $s, t$ over a type $\alpha$ and any predicate $p : \alpha \to \mathrm{Prop}$, the set of elements satisfying both membership in $s$ and $t$ and the predicate $p$ is equal to the intersection of the sets $\{x \in s \mid p x\}$ and $\{x \in t \mid p x\}$. In symbols: $$ \{x \mid (x \in s \land x \in t) \land p x\} = \{x \in s \mid p x\} \cap \{x \in t \mid p x\} $$

Set.sep_and theorem

: {x ∈ s | p x ∧ q x} = {x ∈ s | p x} ∩ {x ∈ s | q x}

Full source

@[simp]
theorem sep_and : { x ∈ s | p x ∧ q x } = { x ∈ s | p x }{ x ∈ s | p x } ∩ { x ∈ s | q x } :=
  inter_inter_distrib_left s {x | p x} {x | q x}

Intersection of Filtered Sets: $\{x \in s \mid p x \land q x\} = \{x \in s \mid p x\} \cap \{x \in s \mid q x\}$

Informal description

For any set $s$ over a type $\alpha$ and predicates $p, q : \alpha \to \text{Prop}$, the set $\{x \in s \mid p x \land q x\}$ is equal to the intersection $\{x \in s \mid p x\} \cap \{x \in s \mid q x\}$.

Set.sep_or theorem

: {x ∈ s | p x ∨ q x} = {x ∈ s | p x} ∪ {x ∈ s | q x}

Full source

@[simp]
theorem sep_or : { x ∈ s | p x ∨ q x } = { x ∈ s | p x }{ x ∈ s | p x } ∪ { x ∈ s | q x } :=
  inter_union_distrib_left s p q

Union of Filtered Sets: $\{x \in s \mid p x \lor q x\} = \{x \in s \mid p x\} \cup \{x \in s \mid q x\}$

Informal description

For any set $s$ over a type $\alpha$ and predicates $p, q : \alpha \to \mathrm{Prop}$, the set $\{x \in s \mid p x \lor q x\}$ is equal to the union $\{x \in s \mid p x\} \cup \{x \in s \mid q x\}$.

Set.sep_setOf theorem

: {x ∈ {y | p y} | q x} = {x | p x ∧ q x}

Full source

@[simp]
theorem sep_setOf : { x ∈ { y | p y } | q x } = { x | p x ∧ q x } :=
  rfl

Separation of Set Comprehension: $\{x \in \{y \mid p y\} \mid q x\} = \{x \mid p x \land q x\}$

Informal description

For any predicates $p$ and $q$ on a type $\alpha$, the set $\{x \in \{y \mid p y\} \mid q x\}$ is equal to the set $\{x \mid p x \land q x\}$.

Set.inter_diff_assoc theorem

(a b c : Set α) : (a ∩ b) \ c = a ∩ (b \ c)

Full source

/-- See also `Set.sdiff_inter_right_comm`. -/
lemma inter_diff_assoc (a b c : Set α) : (a ∩ b) \ c = a ∩ (b \ c) := inf_sdiff_assoc ..

Associativity of Intersection and Set Difference: $(a \cap b) \setminus c = a \cap (b \setminus c)$

Informal description

For any sets $a$, $b$, and $c$ in a type $\alpha$, the set difference $(a \cap b) \setminus c$ is equal to $a \cap (b \setminus c)$.

Set.sdiff_inter_right_comm theorem

(s t u : Set α) : s \ t ∩ u = (s ∩ u) \ t

Full source

/-- See also `Set.inter_diff_assoc`. -/
lemma sdiff_inter_right_comm (s t u : Set α) : s \ ts \ t ∩ u = (s ∩ u) \ t := sdiff_inf_right_comm ..

Set Difference and Intersection Commutativity: $s \setminus (t \cap u) = (s \cap u) \setminus t$

Informal description

For any sets $s$, $t$, and $u$ in a type $\alpha$, the set difference $s \setminus (t \cap u)$ is equal to $(s \cap u) \setminus t$.

Set.inter_sdiff_left_comm theorem

(s t u : Set α) : s ∩ (t \ u) = t ∩ (s \ u)

Full source

lemma inter_sdiff_left_comm (s t u : Set α) : s ∩ (t \ u) = t ∩ (s \ u) := inf_sdiff_left_comm ..

Commutativity of Intersection and Set Difference: $s \cap (t \setminus u) = t \cap (s \setminus u)$

Informal description

For any sets $s$, $t$, and $u$ over a type $\alpha$, the intersection of $s$ with the set difference $t \setminus u$ is equal to the intersection of $t$ with the set difference $s \setminus u$. In other words: $$ s \cap (t \setminus u) = t \cap (s \setminus u) $$

Set.diff_union_diff_cancel theorem

(hts : t ⊆ s) (hut : u ⊆ t) : s \ t ∪ t \ u = s \ u

Full source

theorem diff_union_diff_cancel (hts : t ⊆ s) (hut : u ⊆ t) : s \ ts \ t ∪ t \ u = s \ u :=
  sdiff_sup_sdiff_cancel hts hut

Set Difference Cancellation: $(s \setminus t) \cup (t \setminus u) = s \setminus u$ under $t \subseteq s$ and $u \subseteq t$

Informal description

For any sets $s$, $t$, and $u$ over a type $\alpha$, if $t \subseteq s$ and $u \subseteq t$, then $(s \setminus t) \cup (t \setminus u) = s \setminus u$.

Set.diff_union_diff_cancel' theorem

(hi : s ∩ u ⊆ t) (hu : t ⊆ s ∪ u) : (s \ t) ∪ (t \ u) = s \ u

Full source

/-- A version of `diff_union_diff_cancel` with more general hypotheses. -/
theorem diff_union_diff_cancel' (hi : s ∩ us ∩ u ⊆ t) (hu : t ⊆ s ∪ u) : (s \ t) ∪ (t \ u) = s \ u :=
  sdiff_sup_sdiff_cancel' hi hu

Generalized Set Difference Cancellation: $(s \setminus t) \cup (t \setminus u) = s \setminus u$ under $s \cap u \subseteq t \subseteq s \cup u$

Informal description

For any sets $s$, $t$, and $u$ over a type $\alpha$, if $s \cap u \subseteq t$ and $t \subseteq s \cup u$, then $(s \setminus t) \cup (t \setminus u) = s \setminus u$.

Set.diff_diff_eq_sdiff_union theorem

(h : u ⊆ s) : s \ (t \ u) = s \ t ∪ u

Full source

theorem diff_diff_eq_sdiff_union (h : u ⊆ s) : s \ (t \ u) = s \ ts \ t ∪ u := sdiff_sdiff_eq_sdiff_sup h

Set Difference Identity: $s \setminus (t \setminus u) = (s \setminus t) \cup u$ when $u \subseteq s$

Informal description

For any sets $s$, $t$, and $u$ in a type $\alpha$, if $u \subseteq s$, then the set difference $s \setminus (t \setminus u)$ is equal to the union $(s \setminus t) \cup u$.

Set.inter_diff_distrib_left theorem

(s t u : Set α) : s ∩ (t \ u) = (s ∩ t) \ (s ∩ u)

Full source

theorem inter_diff_distrib_left (s t u : Set α) : s ∩ (t \ u) = (s ∩ t) \ (s ∩ u) :=
  inf_sdiff_distrib_left _ _ _

Left Distributive Law of Intersection over Set Difference

Informal description

For any sets $s$, $t$, and $u$ in a type $\alpha$, the intersection of $s$ with the set difference $t \setminus u$ is equal to the set difference of the intersection $s \cap t$ with the intersection $s \cap u$. In symbols: $$ s \cap (t \setminus u) = (s \cap t) \setminus (s \cap u) $$

Set.inter_diff_distrib_right theorem

(s t u : Set α) : (s \ t) ∩ u = (s ∩ u) \ (t ∩ u)

Full source

theorem inter_diff_distrib_right (s t u : Set α) : (s \ t) ∩ u = (s ∩ u) \ (t ∩ u) :=
  inf_sdiff_distrib_right _ _ _

Right Distributivity of Intersection over Set Difference

Informal description

For any sets $s$, $t$, and $u$ in a type $\alpha$, the intersection of the set difference $s \setminus t$ with $u$ is equal to the set difference of the intersections $(s \cap u) \setminus (t \cap u)$. In symbols: $$(s \setminus t) \cap u = (s \cap u) \setminus (t \cap u).$$

Set.diff_inter_distrib_right theorem

(s t r : Set α) : (t ∩ r) \ s = (t \ s) ∩ (r \ s)

Full source

theorem diff_inter_distrib_right (s t r : Set α) : (t ∩ r) \ s = (t \ s) ∩ (r \ s) :=
  inf_sdiff

Distributivity of Set Difference over Intersection

Informal description

For any sets $s, t, r$ in a type $\alpha$, the set difference of the intersection $t \cap r$ with $s$ is equal to the intersection of the set differences $(t \setminus s) \cap (r \setminus s)$. In other words, $(t \cap r) \setminus s = (t \setminus s) \cap (r \setminus s)$.

Set.compl_def theorem

(s : Set α) : sᶜ = {x | x ∉ s}

Full source

theorem compl_def (s : Set α) : sᶜ = { x | x ∉ s } :=
  rfl

Definition of Set Complement

Informal description

For any set $s$ in a type $\alpha$, the complement $s^c$ is equal to the set $\{x \mid x \notin s\}$.

Set.mem_compl theorem

{s : Set α} {x : α} (h : x ∉ s) : x ∈ sᶜ

Full source

theorem mem_compl {s : Set α} {x : α} (h : x ∉ s) : x ∈ sᶜ :=
  h

Element Not in Set Belongs to Complement

Informal description

For any set $s$ in a type $\alpha$ and any element $x \in \alpha$, if $x$ is not in $s$, then $x$ is in the complement of $s$, i.e., $x \in s^c$.

Set.compl_setOf theorem

{α} (p : α → Prop) : {a | p a}ᶜ = {a | ¬p a}

Full source

theorem compl_setOf {α} (p : α → Prop) : { a | p a }{ a | p a }ᶜ = { a | ¬p a } :=
  rfl

Complement of Set Comprehension Equals Set of Negations

Informal description

For any predicate $p : \alpha \to \text{Prop}$, the complement of the set $\{a \mid p a\}$ is equal to the set $\{a \mid \neg p a\}$.

Set.not_mem_of_mem_compl theorem

{s : Set α} {x : α} (h : x ∈ sᶜ) : x ∉ s

Full source

theorem not_mem_of_mem_compl {s : Set α} {x : α} (h : x ∈ sᶜ) : x ∉ s :=
  h

Complement Membership Implies Non-Membership in Original Set

Informal description

For any set $s$ in a type $\alpha$ and any element $x \in \alpha$, if $x$ belongs to the complement $s^c$, then $x$ does not belong to $s$.

Set.not_mem_compl_iff theorem

{x : α} : x ∉ sᶜ ↔ x ∈ s

Full source

theorem not_mem_compl_iff {x : α} : x ∉ sᶜx ∉ sᶜ ↔ x ∈ s :=
  not_not

Characterization of Non-Membership in Complement Set: $x \notin s^c \leftrightarrow x \in s$

Informal description

For any element $x$ of type $\alpha$ and any set $s$ of elements of $\alpha$, the statement $x \notin s^c$ holds if and only if $x \in s$, where $s^c$ denotes the complement of $s$.

Set.inter_compl_self theorem

(s : Set α) : s ∩ sᶜ = ∅

Full source

@[simp]
theorem inter_compl_self (s : Set α) : s ∩ sᶜ = ∅ :=
  inf_compl_eq_bot

Intersection with Complement is Empty: $s \cap s^c = \emptyset$

Informal description

For any set $s$ in a type $\alpha$, the intersection of $s$ with its complement $s^c$ is the empty set, i.e., $s \cap s^c = \emptyset$.

Set.compl_inter_self theorem

(s : Set α) : sᶜ ∩ s = ∅

Full source

@[simp]
theorem compl_inter_self (s : Set α) : sᶜsᶜ ∩ s = ∅ :=
  compl_inf_eq_bot

Complement Intersection with Set is Empty: $s^c \cap s = \emptyset$

Informal description

For any set $s$ in a type $\alpha$, the intersection of the complement of $s$ with $s$ itself is the empty set, i.e., $s^c \cap s = \emptyset$.

Set.compl_empty theorem

: (∅ : Set α)ᶜ = univ

Full source

@[simp]
theorem compl_empty : (∅ : Set α)ᶜ = univ :=
  compl_bot

Complement of Empty Set is Universal Set: $\emptyset^c = \text{univ}$

Informal description

The complement of the empty set in a type $\alpha$ is equal to the universal set, i.e., $\emptyset^c = \text{univ}$.

Set.compl_union theorem

(s t : Set α) : (s ∪ t)ᶜ = sᶜ ∩ tᶜ

Full source

@[simp]
theorem compl_union (s t : Set α) : (s ∪ t)ᶜ = sᶜsᶜ ∩ tᶜ :=
  compl_sup

De Morgan's Law for Set Complements: $(s \cup t)^c = s^c \cap t^c$

Informal description

For any two sets $s$ and $t$ in a type $\alpha$, the complement of their union equals the intersection of their complements, i.e., $(s \cup t)^c = s^c \cap t^c$.

Set.compl_inter theorem

(s t : Set α) : (s ∩ t)ᶜ = sᶜ ∪ tᶜ

Full source

theorem compl_inter (s t : Set α) : (s ∩ t)ᶜ = sᶜsᶜ ∪ tᶜ :=
  compl_inf

De Morgan's Law for Set Complements: $(s \cap t)^c = s^c \cup t^c$

Informal description

For any two sets $s$ and $t$ in a type $\alpha$, the complement of their intersection equals the union of their complements, i.e., $(s \cap t)^c = s^c \cup t^c$.

Set.compl_univ theorem

: (univ : Set α)ᶜ = ∅

Full source

@[simp]
theorem compl_univ : (univ : Set α)ᶜ = ∅ :=
  compl_top

Complement of Universal Set is Empty: $\alpha^c = \emptyset$

Informal description

The complement of the universal set $\text{univ} = \alpha$ is the empty set $\emptyset$, i.e., $\alpha^c = \emptyset$.

Set.compl_empty_iff theorem

{s : Set α} : sᶜ = ∅ ↔ s = univ

Full source

@[simp]
theorem compl_empty_iff {s : Set α} : sᶜsᶜ = ∅ ↔ s = univ :=
  compl_eq_bot

Complement Equals Empty Set iff Set is Universal

Informal description

For any set $s$ in a type $\alpha$, the complement of $s$ is the empty set if and only if $s$ is the universal set (i.e., $s$ contains all elements of $\alpha$). In symbols: $$ s^c = \emptyset \leftrightarrow s = \text{univ}. $$

Set.compl_univ_iff theorem

{s : Set α} : sᶜ = univ ↔ s = ∅

Full source

@[simp]
theorem compl_univ_iff {s : Set α} : sᶜsᶜ = univ ↔ s = ∅ :=
  compl_eq_top

Complement Equals Universal Set iff Set is Empty

Informal description

For any set $s$ in a type $\alpha$, the complement of $s$ equals the universal set if and only if $s$ is the empty set. In other words, $s^c = \text{univ} \leftrightarrow s = \emptyset$.

Set.compl_ne_univ theorem

: sᶜ ≠ univ ↔ s.Nonempty

Full source

theorem compl_ne_univ : sᶜsᶜ ≠ univsᶜ ≠ univ ↔ s.Nonempty :=
  compl_univ_iff.not.trans nonempty_iff_ne_empty.symm

Nonempty Set Characterization via Complement: $s^c \neq \text{univ} \leftrightarrow s \neq \emptyset$

Informal description

For any set $s$ in a type $\alpha$, the complement $s^c$ is not equal to the universal set if and only if $s$ is nonempty. In other words: $$ s^c \neq \text{univ} \leftrightarrow s \text{ is nonempty}. $$

Set.inl_compl_union_inr_compl theorem

{α β : Type*} {s : Set α} {t : Set β} : Sum.inl '' sᶜ ∪ Sum.inr '' tᶜ = (Sum.inl '' s ∪ Sum.inr '' t)ᶜ

Full source

lemma inl_compl_union_inr_compl {α β : Type*} {s : Set α} {t : Set β} :
    Sum.inlSum.inl '' sᶜSum.inl '' sᶜ ∪ Sum.inr '' tᶜ = (Sum.inl '' s ∪ Sum.inr '' t)ᶜ := by
  rw [compl_union]
  aesop

De Morgan's Law for Complement Images under Sum Injections

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, the union of the image of the complement of $s$ under the left injection $\text{inl} : \alpha \to \alpha \oplus \beta$ and the image of the complement of $t$ under the right injection $\text{inr} : \beta \to \alpha \oplus \beta$ equals the complement of the union of the images of $s$ and $t$ under $\text{inl}$ and $\text{inr}$ respectively. In symbols: $$\text{inl}(s^c) \cup \text{inr}(t^c) = (\text{inl}(s) \cup \text{inr}(t))^c.$$

Set.nonempty_compl theorem

: sᶜ.Nonempty ↔ s ≠ univ

Full source

theorem nonempty_compl : sᶜsᶜ.Nonempty ↔ s ≠ univ :=
  (ne_univ_iff_exists_not_mem s).symm

Nonempty Complement iff Not Universal Set

Informal description

The complement $s^c$ of a set $s$ in a type $\alpha$ is nonempty if and only if $s$ is not equal to the universal set $\text{univ}$ (the set of all elements of $\alpha$).

Set.union_eq_compl_compl_inter_compl theorem

(s t : Set α) : s ∪ t = (sᶜ ∩ tᶜ)ᶜ

Full source

theorem union_eq_compl_compl_inter_compl (s t : Set α) : s ∪ t = (sᶜ ∩ tᶜ)ᶜ :=
  ext fun _ => or_iff_not_and_not

De Morgan's Law for Set Union: $s \cup t = (s^c \cap t^c)^c$

Informal description

For any two sets $s$ and $t$ in a type $\alpha$, the union $s \cup t$ is equal to the complement of the intersection of their complements, i.e., $s \cup t = (s^c \cap t^c)^c$.

Set.inter_eq_compl_compl_union_compl theorem

(s t : Set α) : s ∩ t = (sᶜ ∪ tᶜ)ᶜ

Full source

theorem inter_eq_compl_compl_union_compl (s t : Set α) : s ∩ t = (sᶜ ∪ tᶜ)ᶜ :=
  ext fun _ => and_iff_not_or_not

Intersection as Complement of Union of Complements

Informal description

For any two sets $s$ and $t$ in a type $\alpha$, the intersection $s \cap t$ is equal to the complement of the union of their complements, i.e., $s \cap t = (s^c \cup t^c)^c$.

Set.union_compl_self theorem

(s : Set α) : s ∪ sᶜ = univ

Full source

@[simp]
theorem union_compl_self (s : Set α) : s ∪ sᶜ = univ :=
  eq_univ_iff_forall.2 fun _ => em _

Union with Complement Yields Universal Set

Informal description

For any set $s$ in a type $\alpha$, the union of $s$ with its complement equals the universal set, i.e., $s \cup s^c = \text{univ}$.

Set.compl_union_self theorem

(s : Set α) : sᶜ ∪ s = univ

Full source

@[simp]
theorem compl_union_self (s : Set α) : sᶜsᶜ ∪ s = univ := by rw [union_comm, union_compl_self]

Complement Union with Self Yields Universal Set

Informal description

For any set $s$ in a type $\alpha$, the union of the complement of $s$ with $s$ itself equals the universal set, i.e., $s^c \cup s = \text{univ}$.

Set.compl_subset_comm theorem

: sᶜ ⊆ t ↔ tᶜ ⊆ s

Full source

theorem compl_subset_comm : sᶜsᶜ ⊆ tsᶜ ⊆ t ↔ tᶜ ⊆ s :=
  @compl_le_iff_compl_le _ s _ _

Complement Subset Equivalence: $s^c \subseteq t \leftrightarrow t^c \subseteq s$

Informal description

For any sets $s$ and $t$ in a type $\alpha$, the complement of $s$ is a subset of $t$ if and only if the complement of $t$ is a subset of $s$. That is, $s^c \subseteq t \leftrightarrow t^c \subseteq s$.

Set.subset_compl_comm theorem

: s ⊆ tᶜ ↔ t ⊆ sᶜ

Full source

theorem subset_compl_comm : s ⊆ tᶜs ⊆ tᶜ ↔ t ⊆ sᶜ :=
  @le_compl_iff_le_compl _ _ _ t

Subset-Complement Equivalence: $s \subseteq t^c \leftrightarrow t \subseteq s^c$

Informal description

For any two sets $s$ and $t$ in a type $\alpha$, the set $s$ is a subset of the complement of $t$ if and only if $t$ is a subset of the complement of $s$. In symbols: $$ s \subseteq t^c \leftrightarrow t \subseteq s^c. $$

Set.compl_subset_compl theorem

: sᶜ ⊆ tᶜ ↔ t ⊆ s

Full source

@[simp]
theorem compl_subset_compl : sᶜsᶜ ⊆ tᶜsᶜ ⊆ tᶜ ↔ t ⊆ s :=
  @compl_le_compl_iff_le (Set α) _ _ _

Complement Subset Equivalence: $s^c \subseteq t^c \leftrightarrow t \subseteq s$

Informal description

For any two sets $s$ and $t$ in a type $\alpha$, the complement of $s$ is a subset of the complement of $t$ if and only if $t$ is a subset of $s$. In symbols: $$ s^c \subseteq t^c \leftrightarrow t \subseteq s $$

Set.compl_subset_compl_of_subset theorem

(h : t ⊆ s) : sᶜ ⊆ tᶜ

Full source

@[gcongr] theorem compl_subset_compl_of_subset (h : t ⊆ s) : sᶜsᶜ ⊆ tᶜ := compl_subset_compl.2 h

Complement Reverses Subset Inclusion: $t \subseteq s \implies s^c \subseteq t^c$

Informal description

For any two sets $s$ and $t$ in a type $\alpha$, if $t$ is a subset of $s$, then the complement of $s$ is a subset of the complement of $t$. In symbols: $$ t \subseteq s \implies s^c \subseteq t^c. $$

Set.subset_union_compl_iff_inter_subset theorem

{s t u : Set α} : s ⊆ t ∪ uᶜ ↔ s ∩ u ⊆ t

Full source

theorem subset_union_compl_iff_inter_subset {s t u : Set α} : s ⊆ t ∪ uᶜs ⊆ t ∪ uᶜ ↔ s ∩ u ⊆ t :=
  (@isCompl_compl _ u _).le_sup_right_iff_inf_left_le

Subset-Union-Complement Equivalence via Intersection: $s \subseteq t \cup u^c \leftrightarrow s \cap u \subseteq t$

Informal description

For any sets $s$, $t$, and $u$ of type $\alpha$, the subset relation $s \subseteq t \cup u^c$ holds if and only if the intersection $s \cap u$ is a subset of $t$. In symbols: $$ s \subseteq t \cup u^c \leftrightarrow s \cap u \subseteq t. $$

Set.compl_subset_iff_union theorem

{s t : Set α} : sᶜ ⊆ t ↔ s ∪ t = univ

Full source

theorem compl_subset_iff_union {s t : Set α} : sᶜsᶜ ⊆ tsᶜ ⊆ t ↔ s ∪ t = univ :=
  Iff.symm <| eq_univ_iff_forall.trans <| forall_congr' fun _ => or_iff_not_imp_left

Complement Subset Condition via Union with Universal Set

Informal description

For any two sets $s$ and $t$ in a type $\alpha$, the complement of $s$ is a subset of $t$ if and only if the union of $s$ and $t$ equals the universal set on $\alpha$. In symbols: $$ s^c \subseteq t \leftrightarrow s \cup t = \text{univ}. $$

Set.inter_subset theorem

(a b c : Set α) : a ∩ b ⊆ c ↔ a ⊆ bᶜ ∪ c

Full source

theorem inter_subset (a b c : Set α) : a ∩ ba ∩ b ⊆ ca ∩ b ⊆ c ↔ a ⊆ bᶜ ∪ c :=
  forall_congr' fun _ => and_imp.trans <| imp_congr_right fun _ => imp_iff_not_or

Intersection Subset Relation via Complement and Union: $a \cap b \subseteq c \leftrightarrow a \subseteq b^c \cup c$

Informal description

For any sets $a$, $b$, and $c$ of type $\alpha$, the intersection $a \cap b$ is a subset of $c$ if and only if $a$ is a subset of the union of the complement of $b$ with $c$, i.e., $$ a \cap b \subseteq c \leftrightarrow a \subseteq b^c \cup c. $$

Set.inter_compl_nonempty_iff theorem

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

Full source

theorem inter_compl_nonempty_iff {s t : Set α} : (s ∩ tᶜ).Nonempty ↔ ¬s ⊆ t :=
  (not_subset.trans <| exists_congr fun x => by simp [mem_compl]).symm

Nonempty Intersection with Complement Characterizes Non-Subset Relation

Informal description

For any sets $s$ and $t$ of elements of type $\alpha$, the intersection $s \cap t^c$ is nonempty if and only if $s$ is not a subset of $t$. In other words: $$ s \cap t^c \neq \emptyset \leftrightarrow s \not\subseteq t. $$

Set.not_mem_diff_of_mem theorem

{s t : Set α} {x : α} (hx : x ∈ t) : x ∉ s \ t

Full source

theorem not_mem_diff_of_mem {s t : Set α} {x : α} (hx : x ∈ t) : x ∉ s \ t := fun h => h.2 hx

Non-membership in Set Difference for Elements of Second Set

Informal description

For any sets $s$ and $t$ of type $\alpha$ and any element $x \in \alpha$, if $x \in t$, then $x \notin s \setminus t$.

Set.mem_of_mem_diff theorem

{s t : Set α} {x : α} (h : x ∈ s \ t) : x ∈ s

Full source

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

Element in Set Difference Belongs to First Set

Informal description

For any sets $s$ and $t$ of type $\alpha$ and any element $x \in \alpha$, if $x$ belongs to the set difference $s \setminus t$, then $x$ belongs to $s$.

Set.not_mem_of_mem_diff theorem

{s t : Set α} {x : α} (h : x ∈ s \ t) : x ∉ t

Full source

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

Non-membership in Difference Set

Informal description

For any sets $s, t$ of type $\alpha$ and any element $x \in \alpha$, if $x$ belongs to the set difference $s \setminus t$, then $x$ does not belong to $t$.

Set.diff_eq_compl_inter theorem

{s t : Set α} : s \ t = tᶜ ∩ s

Full source

theorem diff_eq_compl_inter {s t : Set α} : s \ t = tᶜtᶜ ∩ s := by rw [diff_eq, inter_comm]

Set Difference as Intersection with Complement: $s \setminus t = t^c \cap s$

Informal description

For any two sets $s$ and $t$ of elements of type $\alpha$, the set difference $s \setminus t$ is equal to the intersection of the complement of $t$ with $s$, i.e., \[ s \setminus t = t^c \cap s. \]

Set.diff_nonempty theorem

{s t : Set α} : (s \ t).Nonempty ↔ ¬s ⊆ t

Full source

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

Nonempty Difference Characterizes Non-Subset Relation: $s \setminus t \neq \emptyset \leftrightarrow s \not\subseteq t$

Informal description

For any sets $s$ and $t$ of elements of type $\alpha$, the set difference $s \setminus t$ is nonempty if and only if $s$ is not a subset of $t$.

Set.diff_subset theorem

{s t : Set α} : s \ t ⊆ s

Full source

theorem diff_subset {s t : Set α} : s \ ts \ t ⊆ s := show s \ t ≤ s from sdiff_le

Set Difference is Subset of Original Set

Informal description

For any two sets $s$ and $t$ of elements of type $\alpha$, the set difference $s \setminus t$ is a subset of $s$, i.e., \[ s \setminus t \subseteq s. \]

Set.diff_subset_compl theorem

(s t : Set α) : s \ t ⊆ tᶜ

Full source

theorem diff_subset_compl (s t : Set α) : s \ ts \ t ⊆ tᶜ :=
  diff_eq_compl_inter ▸ inter_subset_left

Set Difference is Subset of Complement: $s \setminus t \subseteq t^c$

Informal description

For any two sets $s$ and $t$ over a type $\alpha$, the set difference $s \setminus t$ is a subset of the complement of $t$, i.e., \[ s \setminus t \subseteq t^c. \]

Set.union_diff_cancel' theorem

{s t u : Set α} (h₁ : s ⊆ t) (h₂ : t ⊆ u) : t ∪ u \ s = u

Full source

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

Union-Difference Cancellation under Chain Condition: $t \cup (u \setminus s) = u$ when $s \subseteq t \subseteq u$

Informal description

For any sets $s, t, u$ in a type $\alpha$, if $s \subseteq t$ and $t \subseteq u$, then $t \cup (u \setminus s) = u$.

Set.union_diff_cancel theorem

{s t : Set α} (h : s ⊆ t) : s ∪ t \ s = t

Full source

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

Union-Difference Cancellation: $s \cup (t \setminus s) = t$ when $s \subseteq t$

Informal description

For any two sets $s$ and $t$ in a type $\alpha$, if $s$ is a subset of $t$, then the union of $s$ with the set difference $t \setminus s$ equals $t$, i.e., \[ s \cup (t \setminus s) = t. \]

Set.union_diff_cancel_left theorem

{s t : Set α} (h : s ∩ t ⊆ ∅) : (s ∪ t) \ s = t

Full source

theorem union_diff_cancel_left {s t : Set α} (h : s ∩ ts ∩ t ⊆ ∅) : (s ∪ t) \ s = t :=
  Disjoint.sup_sdiff_cancel_left <| disjoint_iff_inf_le.2 h

Left Union-Difference Cancellation for Disjoint Sets: $(s \cup t) \setminus s = t$ when $s \cap t = \emptyset$

Informal description

For any two sets $s$ and $t$ in a type $\alpha$, if $s$ and $t$ are disjoint (i.e., $s \cap t = \emptyset$), then the set difference of their union with $s$ equals $t$, i.e., \[ (s \cup t) \setminus s = t. \]

Set.union_diff_cancel_right theorem

{s t : Set α} (h : s ∩ t ⊆ ∅) : (s ∪ t) \ t = s

Full source

theorem union_diff_cancel_right {s t : Set α} (h : s ∩ ts ∩ t ⊆ ∅) : (s ∪ t) \ t = s :=
  Disjoint.sup_sdiff_cancel_right <| disjoint_iff_inf_le.2 h

Right Union-Difference Cancellation for Disjoint Sets: $(s \cup t) \setminus t = s$ when $s \cap t = \emptyset$

Informal description

For any two sets $s$ and $t$ in a type $\alpha$, if $s$ and $t$ are disjoint (i.e., $s \cap t = \emptyset$), then the set difference of their union with $t$ equals $s$, i.e., \[ (s \cup t) \setminus t = s. \]

Set.union_diff_left theorem

{s t : Set α} : (s ∪ t) \ s = t \ s

Full source

@[simp]
theorem union_diff_left {s t : Set α} : (s ∪ t) \ s = t \ s :=
  sup_sdiff_left_self

Left Union-Difference Identity for Sets: $(s \cup t) \setminus s = t \setminus s$

Informal description

For any sets $s$ and $t$ over a type $\alpha$, the set difference of their union with $s$ equals the set difference of $t$ with $s$, i.e., $(s \cup t) \setminus s = t \setminus s$.

Set.union_diff_right theorem

{s t : Set α} : (s ∪ t) \ t = s \ t

Full source

@[simp]
theorem union_diff_right {s t : Set α} : (s ∪ t) \ t = s \ t :=
  sup_sdiff_right_self

Right Union-Difference Identity for Sets: $(s \cup t) \setminus t = s \setminus t$

Informal description

For any sets $s$ and $t$ of type $\alpha$, the set difference of their union with $t$ equals the set difference of $s$ with $t$, i.e., $(s \cup t) \setminus t = s \setminus t$.

Set.union_diff_distrib theorem

{s t u : Set α} : (s ∪ t) \ u = s \ u ∪ t \ u

Full source

theorem union_diff_distrib {s t u : Set α} : (s ∪ t) \ u = s \ us \ u ∪ t \ u :=
  sup_sdiff

Distributivity of Set Difference over Union: $(s \cup t) \setminus u = (s \setminus u) \cup (t \setminus u)$

Informal description

For any sets $s, t, u$ over a type $\alpha$, the difference of the union $s \cup t$ with $u$ equals the union of the differences $s \setminus u$ and $t \setminus u$, i.e., $$(s \cup t) \setminus u = (s \setminus u) \cup (t \setminus u).$$

Set.inter_diff_self theorem

(a b : Set α) : a ∩ (b \ a) = ∅

Full source

@[simp]
theorem inter_diff_self (a b : Set α) : a ∩ (b \ a) = ∅ :=
  inf_sdiff_self_right

Intersection with Set Difference Yields Empty Set

Informal description

For any two sets $a$ and $b$ in a type $\alpha$, the intersection of $a$ with the difference of $b$ and $a$ is the empty set, i.e., $a \cap (b \setminus a) = \emptyset$.

Set.inter_union_diff theorem

(s t : Set α) : s ∩ t ∪ s \ t = s

Full source

@[simp]
theorem inter_union_diff (s t : Set α) : s ∩ ts ∩ t ∪ s \ t = s :=
  sup_inf_sdiff s t

Union of Intersection and Difference Equals Original Set

Informal description

For any two sets $s$ and $t$ in a type $\alpha$, the union of their intersection $s \cap t$ and their set difference $s \setminus t$ equals $s$, i.e., $(s \cap t) \cup (s \setminus t) = s$.

Set.diff_union_inter theorem

(s t : Set α) : s \ t ∪ s ∩ t = s

Full source

@[simp]
theorem diff_union_inter (s t : Set α) : s \ ts \ t ∪ s ∩ t = s := by
  rw [union_comm]
  exact sup_inf_sdiff _ _

Decomposition of Set into Difference and Intersection: $(s \setminus t) \cup (s \cap t) = s$

Informal description

For any two sets $s$ and $t$ over a type $\alpha$, the union of the set difference $s \setminus t$ and the intersection $s \cap t$ equals $s$, i.e., $(s \setminus t) \cup (s \cap t) = s$.

Set.inter_union_compl theorem

(s t : Set α) : s ∩ t ∪ s ∩ tᶜ = s

Full source

@[simp]
theorem inter_union_compl (s t : Set α) : s ∩ ts ∩ t ∪ s ∩ tᶜ = s :=
  inter_union_diff _ _

Decomposition of Set via Intersection and Complement: $(s \cap t) \cup (s \cap t^c) = s$

Informal description

For any two sets $s$ and $t$ in a type $\alpha$, the union of their intersection $s \cap t$ and the intersection of $s$ with the complement of $t$ equals $s$, i.e., $(s \cap t) \cup (s \cap t^c) = s$.

Set.diff_subset_diff theorem

{s₁ s₂ t₁ t₂ : Set α} : s₁ ⊆ s₂ → t₂ ⊆ t₁ → s₁ \ t₁ ⊆ s₂ \ t₂

Full source

@[gcongr]
theorem diff_subset_diff {s₁ s₂ t₁ t₂ : Set α} : s₁ ⊆ s₂ → t₂ ⊆ t₁ → s₁ \ t₁s₁ \ t₁ ⊆ s₂ \ t₂ :=
  show s₁ ≤ s₂ → t₂ ≤ t₁ → s₁ \ t₁ ≤ s₂ \ t₂ from sdiff_le_sdiff

Monotonicity of Set Difference: $s₁ \subseteq s₂ \land t₂ \subseteq t₁ \Rightarrow s₁ \setminus t₁ \subseteq s₂ \setminus t₂$

Informal description

For any sets $s₁, s₂, t₁, t₂$ of type $\alpha$, if $s₁ \subseteq s₂$ and $t₂ \subseteq t₁$, then the set difference $s₁ \setminus t₁$ is a subset of $s₂ \setminus t₂$.

Set.diff_subset_diff_left theorem

{s₁ s₂ t : Set α} (h : s₁ ⊆ s₂) : s₁ \ t ⊆ s₂ \ t

Full source

@[gcongr]
theorem diff_subset_diff_left {s₁ s₂ t : Set α} (h : s₁ ⊆ s₂) : s₁ \ ts₁ \ t ⊆ s₂ \ t :=
  sdiff_le_sdiff_right ‹s₁ ≤ s₂›

Monotonicity of Set Difference: $s_1 \subseteq s_2 \Rightarrow s_1 \setminus t \subseteq s_2 \setminus t$

Informal description

For any sets $s_1, s_2, t$ of type $\alpha$, if $s_1 \subseteq s_2$, then the set difference $s_1 \setminus t$ is a subset of $s_2 \setminus t$.

Set.diff_subset_diff_right theorem

{s t u : Set α} (h : t ⊆ u) : s \ u ⊆ s \ t

Full source

@[gcongr]
theorem diff_subset_diff_right {s t u : Set α} (h : t ⊆ u) : s \ us \ u ⊆ s \ t :=
  sdiff_le_sdiff_left ‹t ≤ u›

Monotonicity of Set Difference with Respect to Superset: $t \subseteq u \implies s \setminus u \subseteq s \setminus t$

Informal description

For any sets $s$, $t$, and $u$ of type $\alpha$, if $t \subseteq u$, then the set difference $s \setminus u$ is a subset of $s \setminus t$.

Set.diff_subset_diff_iff_subset theorem

{r : Set α} (hs : s ⊆ r) (ht : t ⊆ r) : r \ s ⊆ r \ t ↔ t ⊆ s

Full source

theorem diff_subset_diff_iff_subset {r : Set α} (hs : s ⊆ r) (ht : t ⊆ r) :
    r \ sr \ s ⊆ r \ tr \ s ⊆ r \ t ↔ t ⊆ s :=
  sdiff_le_sdiff_iff_le hs ht

Set Difference Subset Relation: $r \setminus s \subseteq r \setminus t \leftrightarrow t \subseteq s$ under $s, t \subseteq r$

Informal description

Let $r$, $s$, and $t$ be sets in a type $\alpha$ such that $s \subseteq r$ and $t \subseteq r$. Then the set difference $r \setminus s$ is a subset of $r \setminus t$ if and only if $t$ is a subset of $s$.

Set.compl_eq_univ_diff theorem

(s : Set α) : sᶜ = univ \ s

Full source

theorem compl_eq_univ_diff (s : Set α) : sᶜ = univuniv \ s :=
  top_sdiff.symm

Complement as Universal Set Difference

Informal description

For any set $s$ in a type $\alpha$, the complement of $s$ is equal to the set difference between the universal set and $s$, i.e., $s^c = \text{univ} \setminus s$.

Set.empty_diff theorem

(s : Set α) : (∅ \ s : Set α) = ∅

Full source

@[simp]
theorem empty_diff (s : Set α) : (∅∅ \ s : Set α) = ∅ :=
  bot_sdiff

Empty Set Difference Identity: $\emptyset \setminus s = \emptyset$

Informal description

For any set $s$ of type $\alpha$, the difference between the empty set $\emptyset$ and $s$ is equal to the empty set, i.e., $\emptyset \setminus s = \emptyset$.

Set.diff_eq_empty theorem

{s t : Set α} : s \ t = ∅ ↔ s ⊆ t

Full source

theorem diff_eq_empty {s t : Set α} : s \ ts \ t = ∅ ↔ s ⊆ t :=
  sdiff_eq_bot_iff

Characterization of Empty Set Difference: $s \setminus t = \emptyset \leftrightarrow s \subseteq t$

Informal description

For any two sets $s$ and $t$ over a type $\alpha$, the set difference $s \setminus t$ is equal to the empty set if and only if $s$ is a subset of $t$.

Set.diff_empty theorem

{s : Set α} : s \ ∅ = s

Full source

@[simp]
theorem diff_empty {s : Set α} : s \ ∅ = s :=
  sdiff_bot

Set Difference with Empty Set: $s \setminus \emptyset = s$

Informal description

For any set $s$ of elements of type $\alpha$, the set difference $s \setminus \emptyset$ is equal to $s$.

Set.diff_univ theorem

(s : Set α) : s \ univ = ∅

Full source

@[simp]
theorem diff_univ (s : Set α) : s \ univ = ∅ :=
  diff_eq_empty.2 (subset_univ s)

Set Difference with Universal Set Yields Empty Set: $s \setminus \text{univ} = \emptyset$

Informal description

For any set $s$ of elements of type $\alpha$, the set difference $s \setminus \text{univ}$ is equal to the empty set, where $\text{univ}$ denotes the universal set containing all elements of $\alpha$.

Set.diff_diff theorem

{u : Set α} : (s \ t) \ u = s \ (t ∪ u)

Full source

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

Double Set Difference Equals Difference of Union

Informal description

For any sets $s$, $t$, and $u$ over a type $\alpha$, the double set difference satisfies $(s \setminus t) \setminus u = s \setminus (t \cup u)$.

Set.diff_diff_comm theorem

{s t u : Set α} : (s \ t) \ u = (s \ u) \ t

Full source

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

Commutativity of Double Set Difference

Informal description

For any sets $s, t, u$ in a type $\alpha$, the double set difference operation satisfies $(s \setminus t) \setminus u = (s \setminus u) \setminus t$.

Set.diff_subset_iff theorem

{s t u : Set α} : s \ t ⊆ u ↔ s ⊆ t ∪ u

Full source

theorem diff_subset_iff {s t u : Set α} : s \ ts \ t ⊆ us \ t ⊆ u ↔ s ⊆ t ∪ u :=
  show s \ ts \ t ≤ u ↔ s ≤ t ∪ u from sdiff_le_iff

Characterization of Set Difference via Union: $s \setminus t \subseteq u \leftrightarrow s \subseteq t \cup u$

Informal description

For any sets $s$, $t$, and $u$ of type $\alpha$, the set difference $s \setminus t$ is a subset of $u$ if and only if $s$ is a subset of the union $t \cup u$. In symbols: $$ s \setminus t \subseteq u \leftrightarrow s \subseteq t \cup u $$

Set.subset_diff_union theorem

(s t : Set α) : s ⊆ s \ t ∪ t

Full source

theorem subset_diff_union (s t : Set α) : s ⊆ s \ t ∪ t :=
  show s ≤ s \ ts \ t ∪ t from le_sdiff_sup

Subset Decomposition via Difference and Union: $s \subseteq (s \setminus t) \cup t$

Informal description

For any two sets $s$ and $t$ in a type $\alpha$, the set $s$ is a subset of the union of the set difference $s \setminus t$ and the set $t$, i.e., $s \subseteq (s \setminus t) \cup t$.

Set.diff_union_of_subset theorem

{s t : Set α} (h : t ⊆ s) : s \ t ∪ t = s

Full source

theorem diff_union_of_subset {s t : Set α} (h : t ⊆ s) : s \ ts \ t ∪ t = s :=
  Subset.antisymm (union_subset diff_subset h) (subset_diff_union _ _)

Set Decomposition via Difference and Union: $s \setminus t \cup t = s$ when $t \subseteq s$

Informal description

For any two sets $s$ and $t$ of elements of type $\alpha$, if $t$ is a subset of $s$, then the union of the set difference $s \setminus t$ and $t$ equals $s$, i.e., $$ s \setminus t \cup t = s. $$

Set.diff_subset_comm theorem

{s t u : Set α} : s \ t ⊆ u ↔ s \ u ⊆ t

Full source

theorem diff_subset_comm {s t u : Set α} : s \ ts \ t ⊆ us \ t ⊆ u ↔ s \ u ⊆ t :=
  show s \ ts \ t ≤ u ↔ s \ u ≤ t from sdiff_le_comm

Commutativity of Set Difference Inclusion: $s \setminus t \subseteq u \leftrightarrow s \setminus u \subseteq t$

Informal description

For any sets $s$, $t$, and $u$ of type $\alpha$, the set difference $s \setminus t$ is a subset of $u$ if and only if the set difference $s \setminus u$ is a subset of $t$.

Set.diff_inter theorem

{s t u : Set α} : s \ (t ∩ u) = s \ t ∪ s \ u

Full source

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

Distributivity of Set Difference over Intersection: $s \setminus (t \cap u) = (s \setminus t) \cup (s \setminus u)$

Informal description

For any sets $s$, $t$, and $u$ of a type $\alpha$, the set difference $s \setminus (t \cap u)$ is equal to the union of the set differences $s \setminus t$ and $s \setminus u$. In symbols: $$ s \setminus (t \cap u) = (s \setminus t) \cup (s \setminus u) $$

Set.diff_inter_diff theorem

: s \ t ∩ (s \ u) = s \ (t ∪ u)

Full source

theorem diff_inter_diff : s \ ts \ t ∩ (s \ u) = s \ (t ∪ u) :=
  sdiff_sup.symm

Intersection of Set Differences Equals Difference of Union

Informal description

For any sets $s$, $t$, and $u$ in a type $\alpha$, the intersection of the set differences $s \setminus t$ and $s \setminus u$ equals the set difference $s \setminus (t \cup u)$. In symbols: $$ (s \setminus t) \cap (s \setminus u) = s \setminus (t \cup u) $$

Set.diff_compl theorem

: s \ tᶜ = s ∩ t

Full source

theorem diff_compl : s \ tᶜ = s ∩ t :=
  sdiff_compl

Set Difference with Complement Equals Intersection

Informal description

For any sets $s$ and $t$ in a type $\alpha$, the set difference $s \setminus t^c$ equals the intersection $s \cap t$.

Set.compl_diff theorem

: (t \ s)ᶜ = s ∪ tᶜ

Full source

theorem compl_diff : (t \ s)ᶜ = s ∪ tᶜ :=
  Eq.trans compl_sdiff himp_eq

Complement of Set Difference: $(t \setminus s)^c = s \cup t^c$

Informal description

For any sets $s$ and $t$ over a type $\alpha$, the complement of the set difference $t \setminus s$ is equal to the union of $s$ with the complement of $t$, i.e., $(t \setminus s)^c = s \cup t^c$.

Set.diff_diff_right theorem

{s t u : Set α} : s \ (t \ u) = s \ t ∪ s ∩ u

Full source

theorem diff_diff_right {s t u : Set α} : s \ (t \ u) = s \ ts \ t ∪ s ∩ u :=
  sdiff_sdiff_right'

Double Set Difference Identity: $s \setminus (t \setminus u) = (s \setminus t) \cup (s \cap u)$

Informal description

For any sets $s$, $t$, and $u$ over a type $\alpha$, the set difference $s \setminus (t \setminus u)$ is equal to the union of $s \setminus t$ and $s \cap u$, i.e., $$ s \setminus (t \setminus u) = (s \setminus t) \cup (s \cap u). $$

Set.inter_diff_right_comm theorem

: (s ∩ t) \ u = s \ u ∩ t

Full source

theorem inter_diff_right_comm : (s ∩ t) \ u = s \ us \ u ∩ t := by
  rw [diff_eq, diff_eq, inter_right_comm]

Right Commutativity of Intersection with Set Difference: $(s \cap t) \setminus u = (s \setminus u) \cap t$

Informal description

For any sets $s$, $t$, and $u$ over a type $\alpha$, the set difference $(s \cap t) \setminus u$ is equal to $(s \setminus u) \cap t$.

Set.diff_inter_right_comm theorem

: (s \ u) ∩ t = (s ∩ t) \ u

Full source

theorem diff_inter_right_comm : (s \ u) ∩ t = (s ∩ t) \ u := by
  rw [diff_eq, diff_eq, inter_right_comm]

Commutativity of Set Difference and Intersection: $(s \setminus u) \cap t = (s \cap t) \setminus u$

Informal description

For any sets $s$, $t$, and $u$ over a type $\alpha$, the intersection of the set difference $s \setminus u$ with $t$ is equal to the set difference of the intersection $s \cap t$ with $u$, i.e., $$(s \setminus u) \cap t = (s \cap t) \setminus u.$$

Set.union_diff_self theorem

{s t : Set α} : s ∪ t \ s = s ∪ t

Full source

@[simp]
theorem union_diff_self {s t : Set α} : s ∪ t \ s = s ∪ t :=
  sup_sdiff_self _ _

Union-Difference Identity: $s \cup (t \setminus s) = s \cup t$

Informal description

For any sets $s$ and $t$ over a type $\alpha$, the union of $s$ with the set difference $t \setminus s$ equals the union of $s$ and $t$, i.e., $s \cup (t \setminus s) = s \cup t$.

Set.diff_union_self theorem

{s t : Set α} : s \ t ∪ t = s ∪ t

Full source

@[simp]
theorem diff_union_self {s t : Set α} : s \ ts \ t ∪ t = s ∪ t :=
  sdiff_sup_self _ _

Set Difference-Union Identity: $(s \setminus t) \cup t = s \cup t$

Informal description

For any sets $s$ and $t$ over a type $\alpha$, the union of the set difference $s \setminus t$ with $t$ equals the union of $s$ and $t$, i.e., $$(s \setminus t) \cup t = s \cup t.$$

Set.diff_inter_self theorem

{a b : Set α} : b \ a ∩ a = ∅

Full source

@[simp]
theorem diff_inter_self {a b : Set α} : b \ ab \ a ∩ a = ∅ :=
  inf_sdiff_self_left

Intersection of Set Difference with Original Set is Empty

Informal description

For any two sets $a$ and $b$ over a type $\alpha$, the intersection of the set difference $b \setminus a$ with $a$ is the empty set, i.e., $(b \setminus a) \cap a = \emptyset$.

Set.diff_inter_self_eq_diff theorem

{s t : Set α} : s \ (t ∩ s) = s \ t

Full source

@[simp]
theorem diff_inter_self_eq_diff {s t : Set α} : s \ (t ∩ s) = s \ t :=
  sdiff_inf_self_right _ _

Set Difference Identity: $s \setminus (t \cap s) = s \setminus t$

Informal description

For any sets $s$ and $t$ over a type $\alpha$, the set difference $s \setminus (t \cap s)$ is equal to $s \setminus t$.

Set.diff_self_inter theorem

{s t : Set α} : s \ (s ∩ t) = s \ t

Full source

@[simp]
theorem diff_self_inter {s t : Set α} : s \ (s ∩ t) = s \ t :=
  sdiff_inf_self_left _ _

Set Difference with Intersection Equals Set Difference: $s \setminus (s \cap t) = s \setminus t$

Informal description

For any two sets $s$ and $t$ of elements of type $\alpha$, the set difference $s \setminus (s \cap t)$ is equal to the set difference $s \setminus t$.

Set.diff_self theorem

{s : Set α} : s \ s = ∅

Full source

theorem diff_self {s : Set α} : s \ s = ∅ :=
  sdiff_self

Self-Difference Yields Empty Set: $s \setminus s = \emptyset$

Informal description

For any set $s$ of elements of type $\alpha$, the set difference $s \setminus s$ is equal to the empty set $\emptyset$.

Set.diff_diff_right_self theorem

(s t : Set α) : s \ (s \ t) = s ∩ t

Full source

theorem diff_diff_right_self (s t : Set α) : s \ (s \ t) = s ∩ t :=
  sdiff_sdiff_right_self

Double Set Difference Equals Intersection: $s \setminus (s \setminus t) = s \cap t$

Informal description

For any two sets $s$ and $t$ in a type $\alpha$, the set difference $s \setminus (s \setminus t)$ equals the intersection $s \cap t$.

Set.diff_diff_cancel_left theorem

{s t : Set α} (h : s ⊆ t) : t \ (t \ s) = s

Full source

theorem diff_diff_cancel_left {s t : Set α} (h : s ⊆ t) : t \ (t \ s) = s :=
  sdiff_sdiff_eq_self h

Double Set Difference Cancellation: $t \setminus (t \setminus s) = s$ when $s \subseteq t$

Informal description

For any two sets $s$ and $t$ of elements of type $\alpha$, if $s$ is a subset of $t$ (i.e., $s \subseteq t$), then the set difference $t \setminus (t \setminus s)$ equals $s$.

Set.union_eq_diff_union_diff_union_inter theorem

(s t : Set α) : s ∪ t = s \ t ∪ t \ s ∪ s ∩ t

Full source

theorem union_eq_diff_union_diff_union_inter (s t : Set α) : s ∪ t = s \ ts \ t ∪ t \ ss \ t ∪ t \ s ∪ s ∩ t :=
  sup_eq_sdiff_sup_sdiff_sup_inf

Union Decomposition via Differences and Intersection: $s \cup t = (s \setminus t) \cup (t \setminus s) \cup (s \cap t)$

Informal description

For any two sets $s$ and $t$ in a type $\alpha$, the union $s \cup t$ equals the union of the set differences $s \setminus t$ and $t \setminus s$ together with their intersection $s \cap t$. That is, $$ s \cup t = (s \setminus t) \cup (t \setminus s) \cup (s \cap t). $$

Set.mem_powerset theorem

{x s : Set α} (h : x ⊆ s) : x ∈ 𝒫 s

Full source

theorem mem_powerset {x s : Set α} (h : x ⊆ s) : x ∈ 𝒫 s := @h

Membership in Powerset via Subset Relation

Informal description

For any sets $x$ and $s$ of type $\alpha$, if $x$ is a subset of $s$ (i.e., $x \subseteq s$), then $x$ belongs to the powerset of $s$ (i.e., $x \in \mathcal{P}(s)$).

Set.subset_of_mem_powerset theorem

{x s : Set α} (h : x ∈ 𝒫 s) : x ⊆ s

Full source

theorem subset_of_mem_powerset {x s : Set α} (h : x ∈ 𝒫 s) : x ⊆ s := @h

Membership in Powerset Implies Subset Relation

Informal description

For any sets $x$ and $s$ of type $\alpha$, if $x$ belongs to the powerset of $s$ (i.e., $x \in \mathcal{P}(s)$), then $x$ is a subset of $s$ (i.e., $x \subseteq s$).

Set.mem_powerset_iff theorem

(x s : Set α) : x ∈ 𝒫 s ↔ x ⊆ s

Full source

@[simp]
theorem mem_powerset_iff (x s : Set α) : x ∈ 𝒫 sx ∈ 𝒫 s ↔ x ⊆ s :=
  Iff.rfl

Characterization of Powerset Membership via Subset Relation

Informal description

For any sets $x$ and $s$ of type $\alpha$, $x$ belongs to the powerset of $s$ if and only if $x$ is a subset of $s$, i.e., $x \in \mathcal{P}(s) \leftrightarrow x \subseteq s$.

Set.powerset_inter theorem

(s t : Set α) : 𝒫(s ∩ t) = 𝒫 s ∩ 𝒫 t

Full source

theorem powerset_inter (s t : Set α) : 𝒫(s ∩ t) = 𝒫 s𝒫 s ∩ 𝒫 t :=
  ext fun _ => subset_inter_iff

Powerset of Intersection Equals Intersection of Powersets

Informal description

For any two sets $s$ and $t$ of type $\alpha$, the powerset of their intersection equals the intersection of their powersets, i.e., $\mathcal{P}(s \cap t) = \mathcal{P}(s) \cap \mathcal{P}(t)$.

Set.powerset_mono theorem

: 𝒫 s ⊆ 𝒫 t ↔ s ⊆ t

Full source

@[simp]
theorem powerset_mono : 𝒫 s𝒫 s ⊆ 𝒫 t𝒫 s ⊆ 𝒫 t ↔ s ⊆ t :=
  ⟨fun h => @h _ (fun _ h => h), fun h _ hu _ ha => h (hu ha)⟩

Powerset Monotonicity: $\mathcal{P}(s) \subseteq \mathcal{P}(t) \leftrightarrow s \subseteq t$

Informal description

For any two sets $s$ and $t$ of type $\alpha$, the powerset of $s$ is a subset of the powerset of $t$ if and only if $s$ is a subset of $t$, i.e., $\mathcal{P}(s) \subseteq \mathcal{P}(t) \leftrightarrow s \subseteq t$.

Set.monotone_powerset theorem

: Monotone (powerset : Set α → Set (Set α))

Full source

theorem monotone_powerset : Monotone (powerset : Set α → Set (Set α)) := fun _ _ => powerset_mono.2

Monotonicity of the Powerset Operation

Informal description

The powerset operation $\mathcal{P} : \text{Set } \alpha \to \text{Set } (\text{Set } \alpha)$, which maps a set $s$ to its collection of all subsets, is a monotone function. That is, for any sets $s$ and $t$ of type $\alpha$, if $s \subseteq t$, then $\mathcal{P}(s) \subseteq \mathcal{P}(t)$.

Set.powerset_nonempty theorem

: (𝒫 s).Nonempty

Full source

@[simp]
theorem powerset_nonempty : (𝒫 s).Nonempty :=
  ⟨∅, fun _ h => empty_subset s h⟩

Nonemptiness of Powerset

Informal description

For any set $s$, the powerset $\mathcal{P}(s)$ is nonempty.

Set.powerset_empty theorem

: 𝒫(∅ : Set α) = {∅}

Full source

@[simp]
theorem powerset_empty : 𝒫(∅ : Set α) = {∅} :=
  ext fun _ => subset_empty_iff

Powerset of Empty Set is Singleton of Empty Set

Informal description

The powerset of the empty set is the singleton set containing only the empty set, i.e., $\mathcal{P}(\emptyset) = \{\emptyset\}$.

Set.powerset_univ theorem

: 𝒫(univ : Set α) = univ

Full source

@[simp]
theorem powerset_univ : 𝒫(univ : Set α) = univ :=
  eq_univ_of_forall subset_univ

Powerset of Universal Set Equals Universal Set

Informal description

The powerset of the universal set on a type $\alpha$ is equal to the universal set on the type of sets over $\alpha$, i.e., $\mathcal{P}(\text{univ}) = \text{univ}$.

Set.mem_dite theorem

 (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

Full source

@[deprecated _root_.mem_dite (since := "2025-01-30")]
protected theorem mem_dite (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 :=
  _root_.mem_dite

Membership in Dependent Conditional Set

Informal description

For any proposition $p$ (with a decidability instance), any family of sets $s$ depending on $p$, any family of sets $t$ depending on $\neg p$, and any element $x$ of type $\alpha$, we have: $$x \in \begin{cases} s(h) & \text{if } h : p \\ t(h) & \text{otherwise} \end{cases} \quad \text{if and only if} \quad (\forall h : p, x \in s(h)) \land (\forall h : \neg p, x \in t(h)).$$

Set.mem_dite_univ_right theorem

(p : Prop) [Decidable p] (t : p → Set α) (x : α) : (x ∈ if h : p then t h else univ) ↔ ∀ h : p, x ∈ t h

Full source

theorem mem_dite_univ_right (p : Prop) [Decidable p] (t : p → Set α) (x : α) :
    (x ∈ if h : p then t h else univ) ↔ ∀ h : p, x ∈ t h := by
  simp [mem_dite]

Membership in Conditional Set with Universal Default Case

Informal description

For any proposition $p$ (with a decidability instance), any family of sets $t$ depending on $p$, and any element $x$ of type $\alpha$, we have: $$x \in \begin{cases} t(h) & \text{if } h : p \\ \text{univ} & \text{otherwise} \end{cases} \quad \text{if and only if} \quad \forall h : p, x \in t(h).$$

Set.mem_ite_univ_right theorem

(p : Prop) [Decidable p] (t : Set α) (x : α) : x ∈ ite p t Set.univ ↔ p → x ∈ t

Full source

@[simp]
theorem mem_ite_univ_right (p : Prop) [Decidable p] (t : Set α) (x : α) :
    x ∈ ite p t Set.univx ∈ ite p t Set.univ ↔ p → x ∈ t :=
  mem_dite_univ_right p (fun _ => t) x

Membership in Conditional Set with Universal False Case

Informal description

For any decidable proposition $p$, any set $t$ of type $\alpha$, and any element $x \in \alpha$, we have: $$x \in \begin{cases} t & \text{if } p \\ \text{univ} & \text{otherwise} \end{cases} \quad \text{if and only if} \quad p \to x \in t.$$

Set.mem_dite_univ_left theorem

(p : Prop) [Decidable p] (t : ¬p → Set α) (x : α) : (x ∈ if h : p then univ else t h) ↔ ∀ h : ¬p, x ∈ t h

Full source

theorem mem_dite_univ_left (p : Prop) [Decidable p] (t : ¬p → Set α) (x : α) :
    (x ∈ if h : p then univ else t h) ↔ ∀ h : ¬p, x ∈ t h := by
  split_ifs <;> simp_all

Membership in Conditional Set with Universal True Case

Informal description

For any decidable proposition $p$, any family of sets $t$ depending on $\neg p$, and any element $x$ of type $\alpha$, we have: $$x \in \begin{cases} \text{univ} & \text{if } p \\ t(h) & \text{otherwise} \end{cases} \quad \text{if and only if} \quad \forall h : \neg p, x \in t(h).$$

Set.mem_ite_univ_left theorem

(p : Prop) [Decidable p] (t : Set α) (x : α) : x ∈ ite p Set.univ t ↔ ¬p → x ∈ t

Full source

@[simp]
theorem mem_ite_univ_left (p : Prop) [Decidable p] (t : Set α) (x : α) :
    x ∈ ite p Set.univ tx ∈ ite p Set.univ t ↔ ¬p → x ∈ t :=
  mem_dite_univ_left p (fun _ => t) x

Membership in Conditional Set with Universal True Case (Left Variant)

Informal description

For any decidable proposition $p$, any set $t$ of elements of type $\alpha$, and any element $x \in \alpha$, we have: $$x \in \begin{cases} \text{univ} & \text{if } p \\ t & \text{otherwise} \end{cases} \quad \text{if and only if} \quad \neg p \to x \in t.$$

Set.mem_dite_empty_right theorem

(p : Prop) [Decidable p] (t : p → Set α) (x : α) : (x ∈ if h : p then t h else ∅) ↔ ∃ h : p, x ∈ t h

Full source

theorem mem_dite_empty_right (p : Prop) [Decidable p] (t : p → Set α) (x : α) :
    (x ∈ if h : p then t h else ∅) ↔ ∃ h : p, x ∈ t h := by
  simp only [mem_dite, mem_empty_iff_false, imp_false, not_not]
  exact ⟨fun h => ⟨h.2, h.1 h.2⟩, fun ⟨h₁, h₂⟩ => ⟨fun _ => h₂, h₁⟩⟩

Membership in Conditional Empty Set (Right Case)

Informal description

For any decidable proposition $p$, any family of sets $t$ depending on $p$, and any element $x$ of type $\alpha$, we have: $$x \in \begin{cases} t(h) & \text{if } p \\ \emptyset & \text{otherwise} \end{cases} \quad \text{if and only if} \quad \exists h : p, x \in t(h).$$

Set.mem_ite_empty_right theorem

(p : Prop) [Decidable p] (t : Set α) (x : α) : x ∈ ite p t ∅ ↔ p ∧ x ∈ t

Full source

@[simp]
theorem mem_ite_empty_right (p : Prop) [Decidable p] (t : Set α) (x : α) :
    x ∈ ite p t ∅x ∈ ite p t ∅ ↔ p ∧ x ∈ t :=
  (mem_dite_empty_right p (fun _ => t) x).trans (by simp)

Membership in Conditional Empty Set (Right Case)

Informal description

For any decidable proposition $p$, any set $t$ of elements of type $\alpha$, and any element $x \in \alpha$, we have: $$x \in \begin{cases} t & \text{if } p \\ \emptyset & \text{otherwise} \end{cases} \quad \text{if and only if} \quad p \text{ holds and } x \in t.$$

Set.mem_dite_empty_left theorem

(p : Prop) [Decidable p] (t : ¬p → Set α) (x : α) : (x ∈ if h : p then ∅ else t h) ↔ ∃ h : ¬p, x ∈ t h

Full source

theorem mem_dite_empty_left (p : Prop) [Decidable p] (t : ¬p → Set α) (x : α) :
    (x ∈ if h : p then ∅ else t h) ↔ ∃ h : ¬p, x ∈ t h := by
  simp only [mem_dite, mem_empty_iff_false, imp_false]
  exact ⟨fun h => ⟨h.1, h.2 h.1⟩, fun ⟨h₁, h₂⟩ => ⟨fun h => h₁ h, fun _ => h₂⟩⟩

Membership in Conditional Empty Set (Left Case)

Informal description

For any proposition $p$ with a decidability instance, a function $t : \neg p \to \text{Set } \alpha$, and an element $x \in \alpha$, we have: $$x \in \begin{cases} \emptyset & \text{if } p \\ t(h) & \text{otherwise} \end{cases} \iff \exists h : \neg p, x \in t(h)$$

Set.mem_ite_empty_left theorem

(p : Prop) [Decidable p] (t : Set α) (x : α) : x ∈ ite p ∅ t ↔ ¬p ∧ x ∈ t

Full source

@[simp]
theorem mem_ite_empty_left (p : Prop) [Decidable p] (t : Set α) (x : α) :
    x ∈ ite p ∅ tx ∈ ite p ∅ t ↔ ¬p ∧ x ∈ t :=
  (mem_dite_empty_left p (fun _ => t) x).trans (by simp)

Membership in Conditional Empty Set (Left Case)

Informal description

For any decidable proposition $p$, any set $t$ of elements of type $\alpha$, and any element $x \in \alpha$, we have: $$x \in \begin{cases} \emptyset & \text{if } p \\ t & \text{otherwise} \end{cases} \quad \text{if and only if} \quad \neg p \text{ holds and } x \in t.$$

Set.ite definition

(t s s' : Set α) : Set α

Full source

/-- `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`. -/
protected def ite (t s s' : Set α) : Set α :=
  s ∩ ts ∩ t ∪ s' \ t

If-then-else operation for sets

Informal description

The if-then-else operation for sets, defined as $s \cap t \cup s' \setminus t$, satisfies: 1. $\text{ite}(t, s, s') \cap t = s \cap t$ 2. $\text{ite}(t, s, s') \cap t^c = s' \cap t^c$ where $t^c$ denotes the complement of $t$.

Set.ite_inter_self theorem

(t s s' : Set α) : t.ite s s' ∩ t = s ∩ t

Full source

@[simp]
theorem ite_inter_self (t s s' : Set α) : t.ite s s' ∩ t = s ∩ t := by
  rw [Set.ite, union_inter_distrib_right, diff_inter_self, inter_assoc, inter_self, union_empty]

Intersection Property of If-Then-Else Set: $\text{ite}(t, s, s') \cap t = s \cap t$

Informal description

For any sets $t, s, s'$ over a type $\alpha$, the intersection of the if-then-else set $\text{ite}(t, s, s')$ with $t$ equals the intersection of $s$ with $t$, i.e., $$ \text{ite}(t, s, s') \cap t = s \cap t. $$

Set.ite_compl theorem

(t s s' : Set α) : tᶜ.ite s s' = t.ite s' s

Full source

@[simp]
theorem ite_compl (t s s' : Set α) : tᶜ.ite s s' = t.ite s' s := by
  rw [Set.ite, Set.ite, diff_compl, union_comm, diff_eq]

Complement Symmetry of If-Then-Else Operation on Sets

Informal description

For any sets $t, s, s'$ in a type $\alpha$, the if-then-else operation on the complement $t^c$ satisfies: \[ \text{ite}(t^c, s, s') = \text{ite}(t, s', s). \]

Set.ite_inter_compl_self theorem

(t s s' : Set α) : t.ite s s' ∩ tᶜ = s' ∩ tᶜ

Full source

@[simp]
theorem ite_inter_compl_self (t s s' : Set α) : t.ite s s' ∩ tᶜ = s' ∩ tᶜ := by
  rw [← ite_compl, ite_inter_self]

Complement Intersection Property of If-Then-Else Set: $\text{ite}(t, s, s') \cap t^c = s' \cap t^c$

Informal description

For any sets $t, s, s'$ over a type $\alpha$, the intersection of the if-then-else set $\text{ite}(t, s, s')$ with the complement of $t$ equals the intersection of $s'$ with the complement of $t$, i.e., $$ \text{ite}(t, s, s') \cap t^c = s' \cap t^c. $$

Set.ite_diff_self theorem

(t s s' : Set α) : t.ite s s' \ t = s' \ t

Full source

@[simp]
theorem ite_diff_self (t s s' : Set α) : t.ite s s' \ t = s' \ t :=
  ite_inter_compl_self t s s'

Set Difference Property of If-Then-Else Set: $\text{ite}(t, s, s') \setminus t = s' \setminus t$

Informal description

For any sets $t, s, s'$ over a type $\alpha$, the set difference of the if-then-else set $\text{ite}(t, s, s')$ with $t$ equals the set difference of $s'$ with $t$, i.e., $$ \text{ite}(t, s, s') \setminus t = s' \setminus t. $$

Set.ite_same theorem

(t s : Set α) : t.ite s s = s

Full source

@[simp]
theorem ite_same (t s : Set α) : t.ite s s = s :=
  inter_union_diff _ _

If-then-else Identity: $t.\text{ite}(s, s) = s$

Informal description

For any sets $t$ and $s$ over a type $\alpha$, the if-then-else operation satisfies $t.\text{ite}(s, s) = s$.

Set.ite_left theorem

(s t : Set α) : s.ite s t = s ∪ t

Full source

@[simp]
theorem ite_left (s t : Set α) : s.ite s t = s ∪ t := by simp [Set.ite]

If-then-else Left Identity: $s.\text{ite}(s, t) = s \cup t$

Informal description

For any sets $s$ and $t$ over a type $\alpha$, the if-then-else operation satisfies $s.\text{ite}(s, t) = s \cup t$.

Set.ite_right theorem

(s t : Set α) : s.ite t s = t ∩ s

Full source

@[simp]
theorem ite_right (s t : Set α) : s.ite t s = t ∩ s := by simp [Set.ite]

If-then-else Right Identity: $s.\text{ite}(t, s) = t \cap s$

Informal description

For any sets $s$ and $t$ over a type $\alpha$, the if-then-else operation satisfies $s.\text{ite}(t, s) = t \cap s$.

Set.ite_empty theorem

(s s' : Set α) : Set.ite ∅ s s' = s'

Full source

@[simp]
theorem ite_empty (s s' : Set α) : Set.ite ∅ s s' = s' := by simp [Set.ite]

If-then-else with Empty Condition Yields Else Case: $\text{ite}(\emptyset, s, s') = s'$

Informal description

For any sets $s$ and $s'$ over a type $\alpha$, the if-then-else operation applied to the empty set yields $s'$, i.e., $\text{ite}(\emptyset, s, s') = s'$.

Set.ite_univ theorem

(s s' : Set α) : Set.ite univ s s' = s

Full source

@[simp]
theorem ite_univ (s s' : Set α) : Set.ite univ s s' = s := by simp [Set.ite]

If-then-else with Universal Condition Yields Then Case: $\text{ite}(\text{univ}, s, s') = s$

Informal description

For any sets $s$ and $s'$ over a type $\alpha$, the if-then-else operation applied to the universal set yields $s$, i.e., $\text{ite}(\text{univ}, s, s') = s$.

Set.ite_empty_left theorem

(t s : Set α) : t.ite ∅ s = s \ t

Full source

@[simp]
theorem ite_empty_left (t s : Set α) : t.ite ∅ s = s \ t := by simp [Set.ite]

If-then-else with Empty Left Case Yields Set Difference: $\text{ite}(t, \emptyset, s) = s \setminus t$

Informal description

For any sets $t$ and $s$ over a type $\alpha$, the if-then-else operation applied to $t$ with the empty set as the "then" case and $s$ as the "else" case yields the set difference $s \setminus t$.

Set.ite_empty_right theorem

(t s : Set α) : t.ite s ∅ = s ∩ t

Full source

@[simp]
theorem ite_empty_right (t s : Set α) : t.ite s ∅ = s ∩ t := by simp [Set.ite]

If-then-else with Empty Right Case Yields Intersection: $\text{ite}(t, s, \emptyset) = s \cap t$

Informal description

For any sets $t$ and $s$ over a type $\alpha$, the if-then-else operation applied to $t$ with $s$ as the "then" case and the empty set as the "else" case yields the intersection $s \cap t$.

Set.ite_mono theorem

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

Full source

theorem ite_mono (t : Set α) {s₁ s₁' s₂ s₂' : Set α} (h : s₁ ⊆ s₂) (h' : s₁' ⊆ s₂') :
    t.ite s₁ s₁' ⊆ t.ite s₂ s₂' :=
  union_subset_union (inter_subset_inter_left _ h) (inter_subset_inter_left _ h')

Monotonicity of If-Then-Else Operation on Sets

Informal description

For any set $t$ and sets $s₁, s₁', s₂, s₂'$ over a type $\alpha$, if $s₁ \subseteq s₂$ and $s₁' \subseteq s₂'$, then the if-then-else operation on $t$ satisfies: \[ \text{ite}(t, s₁, s₁') \subseteq \text{ite}(t, s₂, s₂') \] where $\text{ite}(t, s, s') = (s \cap t) \cup (s' \setminus t)$.

Set.ite_subset_union theorem

(t s s' : Set α) : t.ite s s' ⊆ s ∪ s'

Full source

theorem ite_subset_union (t s s' : Set α) : t.ite s s' ⊆ s ∪ s' :=
  union_subset_union inter_subset_left diff_subset

If-then-else set operation is a subset of the union

Informal description

For any sets $t, s, s'$ over a type $\alpha$, the if-then-else operation on sets satisfies: \[ \text{ite}(t, s, s') \subseteq s \cup s' \] where $\text{ite}(t, s, s') = (s \cap t) \cup (s' \setminus t)$.

Set.inter_subset_ite theorem

(t s s' : Set α) : s ∩ s' ⊆ t.ite s s'

Full source

theorem inter_subset_ite (t s s' : Set α) : s ∩ s's ∩ s' ⊆ t.ite s s' :=
  ite_same t (s ∩ s') ▸ ite_mono _ inter_subset_left inter_subset_right

Intersection is Subset of If-Then-Else Operation: $s \cap s' \subseteq \text{ite}(t, s, s')$

Informal description

For any sets $t, s, s'$ over a type $\alpha$, the intersection $s \cap s'$ is a subset of the if-then-else operation on $t$ applied to $s$ and $s'$, i.e., \[ s \cap s' \subseteq \text{ite}(t, s, s') \] where $\text{ite}(t, s, s') = (s \cap t) \cup (s' \setminus t)$.

Set.ite_inter_inter theorem

(t s₁ s₂ s₁' s₂' : Set α) : t.ite (s₁ ∩ s₂) (s₁' ∩ s₂') = t.ite s₁ s₁' ∩ t.ite s₂ s₂'

Full source

theorem ite_inter_inter (t s₁ s₂ s₁' s₂' : Set α) :
    t.ite (s₁ ∩ s₂) (s₁' ∩ s₂') = t.ite s₁ s₁' ∩ t.ite s₂ s₂' := by
  ext x
  simp only [Set.ite, Set.mem_inter_iff, Set.mem_diff, Set.mem_union]
  tauto

Distributivity of If-Then-Else Operation over Intersection

Informal description

For any sets $t, s_1, s_2, s_1', s_2'$ in a type $\alpha$, the if-then-else operation satisfies: \[ t.\text{ite}(s_1 \cap s_2, s_1' \cap s_2') = t.\text{ite}(s_1, s_1') \cap t.\text{ite}(s_2, s_2') \] where $t.\text{ite}(s, s')$ denotes the set $(s \cap t) \cup (s' \setminus t)$.

Set.ite_inter theorem

(t s₁ s₂ s : Set α) : t.ite (s₁ ∩ s) (s₂ ∩ s) = t.ite s₁ s₂ ∩ s

Full source

theorem ite_inter (t s₁ s₂ s : Set α) : t.ite (s₁ ∩ s) (s₂ ∩ s) = t.ite s₁ s₂ ∩ s := by
  rw [ite_inter_inter, ite_same]

Intersection Preservation for If-Then-Else Operation on Sets

Informal description

For any sets $t, s_1, s_2, s$ over a type $\alpha$, the if-then-else operation satisfies: \[ t.\text{ite}(s_1 \cap s, s_2 \cap s) = t.\text{ite}(s_1, s_2) \cap s \] where $t.\text{ite}(s, s')$ denotes the set $(s \cap t) \cup (s' \setminus t)$.

Set.ite_inter_of_inter_eq theorem

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

Full source

theorem ite_inter_of_inter_eq (t : Set α) {s₁ s₂ s : Set α} (h : s₁ ∩ s = s₂ ∩ s) :
    t.ite s₁ s₂ ∩ s = s₁ ∩ s := by rw [← ite_inter, ← h, ite_same]

If-Then-Else Set Operation Preserves Intersection under Equality Condition: $t.\text{ite}(s_1, s_2) \cap s = s_1 \cap s$ when $s_1 \cap s = s_2 \cap s$

Informal description

For any sets $t, s_1, s_2, s$ over a type $\alpha$, if $s_1 \cap s = s_2 \cap s$, then the intersection of the if-then-else set operation $t.\text{ite}(s_1, s_2)$ with $s$ equals $s_1 \cap s$, where $t.\text{ite}(s_1, s_2) = (s_1 \cap t) \cup (s_2 \setminus t)$.

Set.subset_ite theorem

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

Full source

theorem subset_ite {t s s' u : Set α} : u ⊆ t.ite s s'u ⊆ t.ite s s' ↔ u ∩ t ⊆ s ∧ u \ t ⊆ s' := by
  simp only [subset_def, ← forall_and]
  refine forall_congr' fun x => ?_
  by_cases hx : x ∈ t <;> simp [*, Set.ite]

Subset Condition for If-Then-Else Set Operation: $u \subseteq \text{ite}(t, s, s') \leftrightarrow u \cap t \subseteq s \land u \setminus t \subseteq s'$

Informal description

For any sets $t, s, s', u$ in a type $\alpha$, the subset relation $u \subseteq \text{ite}(t, s, s')$ holds if and only if both $u \cap t \subseteq s$ and $u \setminus t \subseteq s'$, where $\text{ite}(t, s, s')$ denotes the if-then-else operation on sets defined as $(s \cap t) \cup (s' \setminus t)$.

Set.ite_eq_of_subset_left theorem

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

Full source

theorem ite_eq_of_subset_left (t : Set α) {s₁ s₂ : Set α} (h : s₁ ⊆ s₂) :
    t.ite s₁ s₂ = s₁ ∪ (s₂ \ t) := by
  ext x
  by_cases hx : x ∈ t <;> simp [*, Set.ite, or_iff_right_of_imp (@h x)]

If-then-else Set Operation with Left Subset Condition: $\text{ite}(t, s_1, s_2) = s_1 \cup (s_2 \setminus t)$ when $s_1 \subseteq s_2$

Informal description

For any sets $t, s_1, s_2$ in a type $\alpha$, if $s_1$ is a subset of $s_2$, then the if-then-else operation on sets satisfies: $$ \text{ite}(t, s_1, s_2) = s_1 \cup (s_2 \setminus t) $$ where $\text{ite}(t, s_1, s_2)$ is defined as $(s_1 \cap t) \cup (s_2 \setminus t)$.

Set.ite_eq_of_subset_right theorem

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

Full source

theorem ite_eq_of_subset_right (t : Set α) {s₁ s₂ : Set α} (h : s₂ ⊆ s₁) :
    t.ite s₁ s₂ = (s₁ ∩ t) ∪ s₂ := by
  ext x
  by_cases hx : x ∈ t <;> simp [*, Set.ite, or_iff_left_of_imp (@h x)]

If-then-else Set Operation with Right Subset Condition: $\text{ite}(t, s₁, s₂) = (s₁ \cap t) \cup s₂$ when $s₂ \subseteq s₁$

Informal description

For any set $t$ and sets $s₁, s₂$ in a type $\alpha$, if $s₂$ is a subset of $s₁$, then the if-then-else operation on sets satisfies: $$ \text{ite}(t, s₁, s₂) = (s₁ \cap t) \cup s₂ $$ where $\text{ite}(t, s₁, s₂)$ is defined as $(s₁ \cap t) \cup (s₂ \setminus t)$.

Function.Injective.nonempty_apply_iff theorem

{f : Set α → Set β} (hf : Injective f) (h2 : f ∅ = ∅) {s : Set α} : (f s).Nonempty ↔ s.Nonempty

Full source

theorem Injective.nonempty_apply_iff {f : Set α → Set β} (hf : Injective f) (h2 : f ∅ = ∅)
    {s : Set α} : (f s).Nonempty ↔ s.Nonempty := by
  rw [nonempty_iff_ne_empty, ← h2, nonempty_iff_ne_empty, hf.ne_iff]

Nonempty Preservation under Injective Set Functions

Informal description

Let $f : \mathcal{P}(\alpha) \to \mathcal{P}(\beta)$ be an injective function between power sets that maps the empty set to the empty set. Then for any subset $s \subseteq \alpha$, the image $f(s)$ is nonempty if and only if $s$ is nonempty.

Subsingleton.set_cases theorem

{p : Set α → Prop} (h0 : p ∅) (h1 : p univ) (s) : p s

Full source

@[elab_as_elim]
theorem set_cases {p : Set α → Prop} (h0 : p ∅) (h1 : p univ) (s) : p s :=
  (s.eq_empty_or_nonempty.elim fun h => h.symm ▸ h0) fun h => (eq_univ_of_nonempty h).symm ▸ h1

Predicate Holds for All Sets if it Holds for Empty and Universal Sets

Informal description

Let $p$ be a predicate on sets over a type $\alpha$. If $p$ holds for the empty set and for the universal set, then $p$ holds for every set $s$ over $\alpha$.

Subsingleton.mem_iff_nonempty theorem

{α : Type*} [Subsingleton α] {s : Set α} {x : α} : x ∈ s ↔ s.Nonempty

Full source

theorem mem_iff_nonempty {α : Type*} [Subsingleton α] {s : Set α} {x : α} : x ∈ sx ∈ s ↔ s.Nonempty :=
  ⟨fun hx => ⟨x, hx⟩, fun ⟨y, hy⟩ => Subsingleton.elim y x ▸ hy⟩

Membership in Subsingleton Sets is Equivalent to Nonemptiness

Informal description

For any type $\alpha$ with at most one element (i.e., a subsingleton), and for any set $s \subseteq \alpha$ and element $x \in \alpha$, the element $x$ belongs to $s$ if and only if $s$ is nonempty.

Set.decidableSdiff instance

[Decidable (a ∈ s)] [Decidable (a ∈ t)] : Decidable (a ∈ s \ t)

Full source

instance decidableSdiff [Decidable (a ∈ s)] [Decidable (a ∈ t)] : Decidable (a ∈ s \ t) :=
  inferInstanceAs (Decidable (a ∈ sa ∈ s ∧ a ∉ t))

Decidability of Set Difference Membership

Informal description

For any type $\alpha$ and sets $s, t \subseteq \alpha$, if membership in $s$ and $t$ is decidable, then membership in the set difference $s \setminus t$ is also decidable.

Set.decidableInter instance

[Decidable (a ∈ s)] [Decidable (a ∈ t)] : Decidable (a ∈ s ∩ t)

Full source

instance decidableInter [Decidable (a ∈ s)] [Decidable (a ∈ t)] : Decidable (a ∈ s ∩ t) :=
  inferInstanceAs (Decidable (a ∈ sa ∈ s ∧ a ∈ t))

Decidability of Intersection Membership

Informal description

For any element $a$ of type $\alpha$ and any sets $s, t$ of elements of $\alpha$, if membership in $s$ and $t$ are both decidable, then membership in their intersection $s \cap t$ is also decidable.

Set.decidableUnion instance

[Decidable (a ∈ s)] [Decidable (a ∈ t)] : Decidable (a ∈ s ∪ t)

Full source

instance decidableUnion [Decidable (a ∈ s)] [Decidable (a ∈ t)] : Decidable (a ∈ s ∪ t) :=
  inferInstanceAs (Decidable (a ∈ sa ∈ s ∨ a ∈ t))

Decidability of Union Set Membership

Informal description

For any element $a$ of type $\alpha$ and any sets $s, t$ of elements of $\alpha$, if membership in $s$ and $t$ are both decidable, then membership in their union $s \cup t$ is also decidable.

Set.decidableCompl instance

[Decidable (a ∈ s)] : Decidable (a ∈ sᶜ)

Full source

instance decidableCompl [Decidable (a ∈ s)] : Decidable (a ∈ sᶜ) :=
  inferInstanceAs (Decidable (a ∉ s))

Decidability of Complement Set Membership

Informal description

For any element $a$ of type $\alpha$ and any set $s$ of elements of $\alpha$, if membership in $s$ is decidable, then membership in the complement $s^c$ is also decidable.

Set.decidableEmptyset instance

: Decidable (a ∈ (∅ : Set α))

Full source

instance decidableEmptyset : Decidable (a ∈ (∅ : Set α)) := Decidable.isFalse (by simp)

Decidability of Empty Set Membership

Informal description

For any element $a$ of type $\alpha$, the proposition $a \in \emptyset$ is decidable.

Set.decidableUniv instance

: Decidable (a ∈ univ)

Full source

instance decidableUniv : Decidable (a ∈ univ) := Decidable.isTrue (by simp)

Decidability of Universal Set Membership

Informal description

For any element $a$ of type $\alpha$, the proposition $a \in \text{univ}$ (i.e., $a$ belongs to the universal set of $\alpha$) is decidable.

Set.decidableInsert instance

[Decidable (a = b)] [Decidable (a ∈ s)] : Decidable (a ∈ insert b s)

Full source

instance decidableInsert [Decidable (a = b)] [Decidable (a ∈ s)] : Decidable (a ∈ insert b s) :=
  inferInstanceAs (Decidable (_ ∨ _))

Decidability of Membership in Inserted Sets

Informal description

For any elements $a, b$ of type $\alpha$ and set $s$ of $\alpha$, if the equality $a = b$ and the membership $a \in s$ are both decidable, then the membership $a \in \text{insert } b \text{ } s$ is decidable.

Set.decidableSetOf instance

(p : α → Prop) [Decidable (p a)] : Decidable (a ∈ {a | p a})

Full source

instance decidableSetOf (p : α → Prop) [Decidable (p a)] : Decidable (a ∈ { a | p a }) := by
  assumption

Decidability of Membership in Predicate-Defined Sets

Informal description

For any predicate $p : \alpha \to \text{Prop}$ and element $a : \alpha$, if $p a$ is decidable, then the membership $a \in \{x \mid p x\}$ is decidable.

Equiv.setSubtypeComm definition

(p : α → Prop) : Set { a : α // p a } ≃ { s : Set α // ∀ a ∈ s, p a }

Full source

/-- Given a predicate `p : α → Prop`, produces an equivalence between
  `Set {a : α // p a}` and `{s : Set α // ∀ a ∈ s, p a}`. -/
protected def setSubtypeComm (p : α → Prop) :
    SetSet {a : α // p a} ≃ {s : Set α // ∀ a ∈ s, p a} where
  toFun s := ⟨{a | ∃ h : p a, s ⟨a, h⟩}, fun _ h ↦ h.1⟩
  invFun s := {a | a.val ∈ s.val}
  left_inv s := by ext a; exact ⟨fun h ↦ h.2, fun h ↦ ⟨a.property, h⟩⟩
  right_inv s := by ext; exact ⟨fun h ↦ h.2, fun h ↦ ⟨s.property _ h, h⟩⟩

Equivalence between sets of a subtype and restricted subsets

Informal description

Given a predicate $p : \alpha \to \text{Prop}$, there is a natural equivalence between the type of sets over the subtype $\{a : \alpha \mid p a\}$ and the type of subsets $s$ of $\alpha$ where every element $a \in s$ satisfies $p a$. More precisely, the equivalence maps: - A set $S$ of elements $\langle a, h \rangle$ in $\{a : \alpha \mid p a\}$ to the subset $\{a \mid \exists h : p a, \langle a, h \rangle \in S\}$ of $\alpha$, ensuring all elements satisfy $p$. - Conversely, a subset $s$ of $\alpha$ where $\forall a \in s, p a$ holds is mapped to the set $\{\langle a, h \rangle \mid a \in s\}$ in $\{a : \alpha \mid p a\}$.

Equiv.setSubtypeComm_apply theorem

 (p : α → Prop) (s : Set { a // p a }) : (Equiv.setSubtypeComm p) s = ⟨{a | ∃ h : p a, ⟨a, h⟩ ∈ s}, fun _ h ↦ h.1⟩

Full source

@[simp]
protected lemma setSubtypeComm_apply (p : α → Prop) (s : Set {a // p a}) :
    (Equiv.setSubtypeComm p) s = ⟨{a | ∃ h : p a, ⟨a, h⟩ ∈ s}, fun _ h ↦ h.1⟩ :=
  rfl

Application of the Subtype-Set Equivalence: $\mathrm{setSubtypeComm}\, p\, S = \langle \{a \mid \exists h, \langle a, h \rangle \in S\}, \text{proof}\rangle$

Informal description

Given a predicate $p : \alpha \to \mathrm{Prop}$ and a set $S$ of elements in the subtype $\{a : \alpha \mid p a\}$, the equivalence $\mathrm{setSubtypeComm}\, p$ maps $S$ to the pair $\langle \{a \mid \exists h : p a, \langle a, h \rangle \in S\}, \text{proof}\rangle$, where the proof ensures that every element in the resulting set satisfies $p$.

Equiv.setSubtypeComm_symm_apply theorem

(p : α → Prop) (s : { s // ∀ a ∈ s, p a }) : (Equiv.setSubtypeComm p).symm s = {a | a.val ∈ s.val}

Full source

@[simp]
protected lemma setSubtypeComm_symm_apply (p : α → Prop) (s : {s // ∀ a ∈ s, p a}) :
    (Equiv.setSubtypeComm p).symm s = {a | a.val ∈ s.val} :=
  rfl

Inverse Application of Subtype-Set Equivalence: $\mathrm{setSubtypeComm}^{-1}\, p\, s = \{a \mid a \in s\}$

Informal description

Given a predicate $p : \alpha \to \mathrm{Prop}$ and a subset $s$ of $\alpha$ where every element $a \in s$ satisfies $p a$, the inverse of the equivalence $\mathrm{setSubtypeComm}\, p$ maps $s$ to the set $\{a \mid a \in s\}$ in the subtype $\{a : \alpha \mid p a\}$.

Mathlib.Data.Set.Basic

Main definitions

Notation

Implementation notes

Tags