Documentation

MathlibMini.Set.Operations

Sets: Operations #

The empty set, the universal set, singletons, insertion, union, and intersection, each with its membership lemma, and the basic order lemmas relating them to the subset relation.

Inspired by Mathlib's Set. This is an independent, unofficial library.

source
@[instance_reducible]
instance MathlibMini.Set.instEmptyCollection {α : Type u} :
EmptyCollection (Set α)
Equations
source
@[instance_reducible]
instance MathlibMini.Set.instSingleton {α : Type u} :
Singleton α (Set α)
Equations
source
@[instance_reducible]
instance MathlibMini.Set.instInsert {α : Type u} :
Insert α (Set α)
Equations
source
@[instance_reducible]
instance MathlibMini.Set.instUnion {α : Type u} :
Union (Set α)
Equations
source
@[instance_reducible]
instance MathlibMini.Set.instInter {α : Type u} :
Inter (Set α)
Equations
source
def MathlibMini.Set.univ {α : Type u} :
Set α

The set of all elements of α.

Equations
Instances For

    Membership #

    source
    @[simp]
    theorem MathlibMini.Set.mem_empty_iff_false {α : Type u} (element : α) :
    element ∈ ∅ ↔ False

    No element is a member of the empty set.

    source
    @[simp]
    theorem MathlibMini.Set.mem_univ {α : Type u} (element : α) :
    element ∈ univ

    Every element is a member of the universal set.

    source
    @[simp]
    theorem MathlibMini.Set.mem_singleton_iff {α : Type u} {element other : α} :
    other ∈ {element} ↔ other = element

    Membership in a singleton is equality with its element.

    source
    @[simp]
    theorem MathlibMini.Set.mem_insert_iff {α : Type u} {element other : α} {set : Set α} :
    other ∈ insert element set ↔ other = element ∨ other ∈ set

    Membership after insertion is equality with the inserted element or membership in the original set.

    source
    @[simp]
    theorem MathlibMini.Set.mem_union_iff {α : Type u} {left right : Set α} {element : α} :
    element ∈ left ∪ right ↔ element ∈ left ∨ element ∈ right

    Membership in a union is membership in either set.

    source
    @[simp]
    theorem MathlibMini.Set.mem_inter_iff {α : Type u} {left right : Set α} {element : α} :
    element ∈ left ∩ right ↔ element ∈ left ∧ element ∈ right

    Membership in an intersection is membership in both sets.

    Order #

    source
    theorem MathlibMini.Set.empty_subset {α : Type u} (set : Set α) :
    ∅ ⊆ set

    The empty set is a subset of every set.

    source
    theorem MathlibMini.Set.subset_univ {α : Type u} (set : Set α) :
    set ⊆ univ

    Every set is a subset of the universal set.

    source
    theorem MathlibMini.Set.subset_union_left {α : Type u} (left right : Set α) :
    left ⊆ left ∪ right

    A set is a subset of its union with another set, on the left.

    source
    theorem MathlibMini.Set.subset_union_right {α : Type u} (left right : Set α) :
    right ⊆ left ∪ right

    A set is a subset of its union with another set, on the right.

    source
    theorem MathlibMini.Set.union_subset {α : Type u} {left right set : Set α} (h₁ : left ⊆ set) (h₂ : right ⊆ set) :
    left ∪ right ⊆ set

    A union is a subset of a set when both parts are.

    source
    theorem MathlibMini.Set.inter_subset_left {α : Type u} (left right : Set α) :
    left ∩ right ⊆ left

    An intersection is a subset of its left set.

    source
    theorem MathlibMini.Set.inter_subset_right {α : Type u} (left right : Set α) :
    left ∩ right ⊆ right

    An intersection is a subset of its right set.

    source
    theorem MathlibMini.Set.subset_inter {α : Type u} {left right set : Set α} (h₁ : set ⊆ left) (h₂ : set ⊆ right) :
    set ⊆ left ∩ right

    A set is a subset of an intersection when it is a subset of both parts.

    Union laws #

    source
    theorem MathlibMini.Set.union_comm {α : Type u} (left right : Set α) :
    left ∪ right = right ∪ left

    Union is commutative.

    source
    theorem MathlibMini.Set.union_assoc {α : Type u} (first second third : Set α) :
    first ∪ second ∪ third = first ∪ (second ∪ third)

    Union is associative.

    source
    @[simp]
    theorem MathlibMini.Set.union_self {α : Type u} (set : Set α) :
    set ∪ set = set

    A set united with itself is itself.

    source
    @[simp]
    theorem MathlibMini.Set.union_empty {α : Type u} (set : Set α) :
    set ∪ ∅ = set

    The empty set is a right identity for union.

    source
    @[simp]
    theorem MathlibMini.Set.empty_union {α : Type u} (set : Set α) :
    ∅ ∪ set = set

    The empty set is a left identity for union.

    Intersection laws #

    source
    theorem MathlibMini.Set.inter_comm {α : Type u} (left right : Set α) :
    left ∩ right = right ∩ left

    Intersection is commutative.

    source
    @[simp]
    theorem MathlibMini.Set.inter_self {α : Type u} (set : Set α) :
    set ∩ set = set

    A set intersected with itself is itself.