Sets: Basic

The type of sets over a type α, represented by membership predicates.

A set of elements of α is a function α → Prop. No finiteness, enumeration, or decidable membership is assumed.

This module provides the type, construction from a predicate, membership, the subset and strict subset relations, and extensionality. It depends only on Lean core.

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

def MathlibMini.Set (α : Type u) : Type u

A set of elements of α, represented by its membership predicate.

Equations

• MathlibMini.Set α = (α → Prop)

def MathlibMini.Set.ofPredicate {α : Type u} (predicate : α → Prop) : Set α

The set of exactly those elements that satisfy a predicate.

Equations

• MathlibMini.Set.ofPredicate predicate = predicate

@[instance_reducible]

instance MathlibMini.Set.instMembership {α : Type u} : Membership α (Set α)

Equations

• MathlibMini.Set.instMembership = { mem := fun (set : MathlibMini.Set α) (element : α) => set element }

@[instance_reducible]

instance MathlibMini.Set.instHasSubset {α : Type u} : HasSubset (Set α)

Equations

• MathlibMini.Set.instHasSubset = { Subset := fun (left right : MathlibMini.Set α) => ∀ ⦃element : α⦄, element ∈ left → element ∈ right }

@[instance_reducible]

instance MathlibMini.Set.instHasSSubset {α : Type u} : HasSSubset (Set α)

Equations

• MathlibMini.Set.instHasSSubset = { SSubset := fun (left right : MathlibMini.Set α) => left ⊆ right ∧ ¬right ⊆ left }

@[simp]

theorem MathlibMini.Set.mem_ofPredicate_iff {α : Type u} {predicate : α → Prop} {element : α} : element ∈ ofPredicate predicate ↔ predicate element

An element is a member of ofPredicate predicate exactly when it satisfies predicate.

theorem MathlibMini.Set.subset_def {α : Type u} {left right : Set α} : left ⊆ right ↔ ∀ ⦃element : α⦄, element ∈ left → element ∈ right

left ⊆ right unfolds to: every member of left is a member of right.

theorem MathlibMini.Set.ssubset_def {α : Type u} {left right : Set α} : left ⊂ right ↔ left ⊆ right ∧ ¬right ⊆ left

left ⊂ right unfolds to: left ⊆ right and not right ⊆ left.

theorem MathlibMini.Set.ext {α : Type u} {left right : Set α} (h : ∀ (element : α), element ∈ left ↔ element ∈ right) : left = right

Two sets are equal when they have the same members.

theorem MathlibMini.Set.ext_iff {α : Type u} {left right : Set α} : left = right ↔ ∀ (element : α), element ∈ left ↔ element ∈ right

theorem MathlibMini.Set.subset_refl {α : Type u} (set : Set α) : set ⊆ set

Every set is a subset of itself.

theorem MathlibMini.Set.subset_trans {α : Type u} {first second third : Set α} (h₁ : first ⊆ second) (h₂ : second ⊆ third) : first ⊆ third

The subset relation is transitive.

theorem MathlibMini.Set.subset_antisymm {α : Type u} {left right : Set α} (h₁ : left ⊆ right) (h₂ : right ⊆ left) : left = right

Sets that are subsets of each other are equal.