bookshelf/Common/Set/Basic.lean

import Mathlib.Data.Set.Basic

/-! # Common.Set.Basic

Additional theorems and definitions useful in the context of `Set`s.
-/

namespace Set

/-
The Minkowski sum of two sets `s` and `t` is the set
`s + t = { a + b : a ∈ s, b ∈ t }`.
-/
def minkowskiSum {α : Type u} [Add α] (s t : Set α) :=
  { x | ∃ a ∈ s, ∃ b ∈ t, x = a + b }

/--
The sum of two sets is nonempty **iff** the summands are nonempty.
-/
theorem nonempty_minkowski_sum_iff_nonempty_add_nonempty {α : Type u} [Add α]
  {s t : Set α}
  : (minkowskiSum s t).Nonempty ↔ s.Nonempty ∧ t.Nonempty := by
  apply Iff.intro
  · intro h
    have ⟨x, hx⟩ := h
    have ⟨a, ⟨ha, ⟨b, ⟨hb, _⟩⟩⟩⟩ := hx
    apply And.intro
    · exact ⟨a, ha⟩
    · exact ⟨b, hb⟩
  · intro ⟨⟨a, ha⟩, ⟨b, hb⟩⟩
    exact ⟨a + b, ⟨a, ⟨ha, ⟨b, ⟨hb, rfl⟩⟩⟩⟩⟩

/--
The characteristic function of a set `S`.

It returns `1` if the specified input belongs to `S` and `0` otherwise.
-/
def characteristic (S : Set α) (x : α) [Decidable (x ∈ S)] : Nat :=
  if x ∈ S then 1 else 0

end Set
-												Generalize set functions and move partitions in anticipation
of Apostol 1.11 exercise 8.

											
										
										
											2023-05-12 13:05:31 +00:00
+								import Mathlib.Data.Set.Basic
-												Apostol I 3.

Better organize concepts in `common` and continue adding more to parts
of I 3 proofs.

											
										
										
											2023-04-11 12:46:59 +00:00
-												Generalize set functions and move partitions in anticipation
of Apostol 1.11 exercise 8.

											
										
										
											2023-05-12 13:05:31 +00:00
+								/-! # Common.Set.Basic
-												Add documentation throughout modules.

											
										
										
											2023-05-04 22:37:54 +00:00
-												Derive a more constructive `StepFunction` definition.

											
										
										
											2023-05-15 14:00:01 +00:00
+								Additional theorems and definitions useful in the context of `Set`s.
-												Add documentation throughout modules.

											
										
										
											2023-05-04 22:37:54 +00:00
+								-/
-												Generalize set functions and move partitions in anticipation
of Apostol 1.11 exercise 8.

											
										
										
											2023-05-12 13:05:31 +00:00
+								namespace Set
-												Apostol I 3.

Better organize concepts in `common` and continue adding more to parts
of I 3 proofs.

											
										
										
											2023-04-11 12:46:59 +00:00
-												Generalize set functions and move partitions in anticipation
of Apostol 1.11 exercise 8.

											
										
										
											2023-05-12 13:05:31 +00:00
+								/-
-												Apostol I 3.

Better organize concepts in `common` and continue adding more to parts
of I 3 proofs.

											
										
										
											2023-04-11 12:46:59 +00:00
+								The Minkowski sum of two sets `s` and `t` is the set
 								`s + t = { a + b : a ∈ s, b ∈ t }`.
 								-/
-												Use a consistent naming convention.

											
										
										
											2023-05-12 17:08:18 +00:00
+								def minkowskiSum {α : Type u} [Add α] (s t : Set α) :=
-												Apostol I 3.

Better organize concepts in `common` and continue adding more to parts
of I 3 proofs.

											
										
										
											2023-04-11 12:46:59 +00:00
+								  { x | ∃ a ∈ s, ∃ b ∈ t, x = a + b }
-												Apostol. Finish proving additive property of supremums.

											
										
										
											2023-04-13 19:58:38 +00:00
+								/--
-												Add documentation throughout modules.

											
										
										
											2023-05-04 22:37:54 +00:00
+								The sum of two sets is nonempty **iff** the summands are nonempty.
-												Apostol. Finish proving additive property of supremums.

											
										
										
											2023-04-13 19:58:38 +00:00
+								-/
-												Generalize set functions and move partitions in anticipation
of Apostol 1.11 exercise 8.

											
										
										
											2023-05-12 13:05:31 +00:00
+								theorem nonempty_minkowski_sum_iff_nonempty_add_nonempty {α : Type u} [Add α]
 								  {s t : Set α}
-												Use a consistent naming convention.

											
										
										
											2023-05-12 17:08:18 +00:00
+								  : (minkowskiSum s t).Nonempty ↔ s.Nonempty ∧ t.Nonempty := by
-												Apostol. Finish proving additive property of supremums.

											
										
										
											2023-04-13 19:58:38 +00:00
+								  apply Iff.intro
 								  · intro h
 								    have ⟨x, hx⟩ := h
 								    have ⟨a, ⟨ha, ⟨b, ⟨hb, _⟩⟩⟩⟩ := hx
 								    apply And.intro
 								    · exact ⟨a, ha⟩
 								    · exact ⟨b, hb⟩
 								  · intro ⟨⟨a, ha⟩, ⟨b, hb⟩⟩
 								    exact ⟨a + b, ⟨a, ⟨ha, ⟨b, ⟨hb, rfl⟩⟩⟩⟩⟩
-												Generalize set functions and move partitions in anticipation
of Apostol 1.11 exercise 8.

											
										
										
											2023-05-12 13:05:31 +00:00
+								/--
 								The characteristic function of a set `S`.
 								It returns `1` if the specified input belongs to `S` and `0` otherwise.
 								-/
-												Generalize concept of partitions and step functions.

											
										
										
											2023-05-12 19:17:34 +00:00
+								def characteristic (S : Set α) (x : α) [Decidable (x ∈ S)] : Nat :=
-												Generalize set functions and move partitions in anticipation
of Apostol 1.11 exercise 8.

											
										
										
											2023-05-12 13:05:31 +00:00
+								  if x ∈ S then 1 else 0
 								end Set