Set

This file introduces a very basic Set type, which is merely a function from the element type into Prop.

def Set (α : Type u) : Type u

Equations

• Set α = (α → Prop)

@[implicit_reducible]

instance instEmptyCollectionSet {α : Type u_1} : EmptyCollection (Set α)

Equations

• instEmptyCollectionSet = { emptyCollection := fun (x : α) => False }

@[implicit_reducible]

instance instMembershipSet {α : Type u_1} : Membership α (Set α)

Equations

• instMembershipSet = { mem := fun (S : Set α) (a : α) => S a }

@[implicit_reducible]

instance instUnionSet {α : Type u_1} : Union (Set α)

Equations

• instUnionSet = { union := fun (A B : Set α) (e : α) => e ∈ A ∨ e ∈ B }

@[implicit_reducible]

instance instHasSubsetSet {α : Type u_1} : HasSubset (Set α)

Equations

• instHasSubsetSet = { Subset := fun (A B : Set α) => ∀ (e : α), e ∈ A → e ∈ B }

@[implicit_reducible]

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

Equations

• instHasSSubsetSet = { SSubset := fun (A B : Set α) => A ⊆ B ∧ ¬B ⊆ A }

theorem Set.ext {α : Type u_1} (X Y : Set α) : (∀ (e : α), e ∈ X ↔ e ∈ Y) → X = Y

Two sets are the same if they feature the same elements.

theorem Set.ext_iff {α : Type u_1} {X Y : Set α} : X = Y ↔ ∀ (e : α), e ∈ X ↔ e ∈ Y

theorem Set.not_empty_contains_element {α : Type u_1} (X : Set α) : X ≠ ∅ → ∃ (e : α), e ∈ X

A non-empty set contains at least one element.

theorem Set.mem_of_subset_of_mem {α : Type u_1} {e : α} {A B : Set α} : A ⊆ B → e ∈ A → e ∈ B

If A is a subset of B and e is in A, then e is in B. This is essentially the subset definition.

theorem Set.mem_union_iff {α : Type u_1} {e : α} {A B : Set α} : e ∈ A ∪ B ↔ e ∈ A ∨ e ∈ B

Unfolds the definition of set union.

theorem Set.mem_union_of_mem_left {α : Type u_1} {e : α} {A B : Set α} : e ∈ A → e ∈ A ∪ B

If e is in A, then e is in A ∪ B.

theorem Set.mem_union_of_mem_right {α : Type u_1} {e : α} {A B : Set α} : e ∈ B → e ∈ A ∪ B

If e is in B, then e is in A ∪ B.

def Set.map {α : Type u_1} {β : Type u_2} (X : Set α) (f : α → β) : Set β

Apply a mapping function to each member of a set yielding a new set; think of List.map.

Equations

• X.map f e = ∃ (e' : α), e' ∈ X ∧ f e' = e

@[simp]

theorem Set.mem_map {α : Type u_1} {β : Type u_2} {X : Set α} {f : α → β} {e : β} : e ∈ X.map f ↔ ∃ (e' : α), e' ∈ X ∧ f e' = e

This is essentially the definition of map.

theorem Set.mem_map_of_mem {α : Type u_1} {β : Type u_2} {e : α} {X : Set α} {f : α → β} : e ∈ X → f e ∈ X.map f

For a set element, the mapped version of the element is in the mapped set.

theorem Set.subset_refl {α : Type u_1} {X : Set α} : X ⊆ X

The subset relation on sets is reflexive.

theorem Set.subset_trans {α : Type u_1} {a b c : Set α} : a ⊆ b → b ⊆ c → a ⊆ c

The subset relation on sets is transitive.

theorem Set.subset_union_of_subset_left {α : Type u_1} {a b c : Set α} : a ⊆ b → a ⊆ b ∪ c

When a is a subset of b, then a is still a subset of the union of b with c.

theorem Set.subset_union_of_subset_right {α : Type u_1} (a b c : Set α) : a ⊆ c → a ⊆ b ∪ c

When a is a subset of c, then a is still a subset of the union of b with c.

@[simp]

theorem Set.union_subset_iff_both_subset {α : Type u_1} (a b c : Set α) : a ∪ b ⊆ c ↔ a ⊆ c ∧ b ⊆ c

The union of a and b is a subset of c if and only if a and b are both subsets of c.