bookshelf/Common/Set/Basic.lean

356 lines
9.6 KiB
Plaintext
Raw Blame History

This file contains ambiguous Unicode characters!

This file contains ambiguous Unicode characters that may be confused with others in your current locale. If your use case is intentional and legitimate, you can safely ignore this warning. Use the Escape button to highlight these characters.

import Common.Logic.Basic
import Mathlib.Data.Set.Basic
import Mathlib.Data.Set.Prod
import Mathlib.Tactic.LibrarySearch
/-! # Common.Set.Basic
Additional theorems and definitions useful in the context of `Set`s.
-/
namespace Set
/-! ## Minkowski Sum -/
/-
The Minkowski sum of two `Set`s `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 `Set`s 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⟩⟩⟩⟩⟩
/-! ## Pair Sets -/
/--
If `{x, y} = {x}` then `x = y`.
-/
theorem pair_eq_singleton_mem_imp_eq_self {x y : α}
(h : {x, y} = ({x} : Set α)) : y = x := by
rw [Set.ext_iff] at h
have := h y
simp at this
exact this
/--
If `{x, y} = {z}` then `x = y = z`.
-/
theorem pair_eq_singleton_mem_imp_eq_all {x y z : α}
(h : {x, y} = ({z} : Set α)) : x = z ∧ y = z := by
have h' := h
rw [Set.ext_iff] at h'
have hz := h' z
simp at hz
apply Or.elim hz
· intro hzx
rw [← hzx] at h
have := pair_eq_singleton_mem_imp_eq_self h
exact ⟨hzx.symm, this⟩
· intro hzy
rw [← hzy, Set.pair_comm] at h
have := pair_eq_singleton_mem_imp_eq_self h
exact ⟨this, hzy.symm⟩
/-! ## Subsets -/
/--
There exists no proper subset of `∅`.
-/
theorem ssubset_empty_iff_false (S : Set α)
: S ⊂ ∅ ↔ False := by
apply Iff.intro
· intro h
rw [ssubset_iff_subset_ne, subset_empty_iff] at h
exact absurd h.left h.right
· simp only [IsEmpty.forall_iff]
/--
If `Set` `A` is a subset of `Set` `B`, then `A B = B`.
-/
theorem left_subset_union_eq_self {A B : Set α} (h : A ⊆ B)
: A B = B := by
rw [Set.ext_iff]
intro x
apply Iff.intro
· intro hU
apply Or.elim hU
· intro hA
exact h hA
· simp
· intro hB
exact Or.inr hB
/--
If `Set` `B` is a subset of `Set` `A`, then `A B = B`.
-/
theorem right_subset_union_eq_self {A B : Set α} (h : B ⊆ A)
: A B = A := by
rw [Set.union_comm]
exact left_subset_union_eq_self h
/--
If `x` and `y` are members of `Set` `A`, it follows `{x, y}` is a subset of `A`.
-/
theorem mem_mem_imp_pair_subset {x y : α}
(hx : x ∈ A) (hy : y ∈ A) : ({x, y} : Set α) ⊆ A := by
intro a ha
apply Or.elim ha
· intro hx'
rwa [hx']
· intro hy'
rwa [hy']
/-! ## Powerset -/
/--
Every `Set` is a member of its own powerset.
-/
theorem self_mem_powerset_self {A : Set α}
: A ∈ 𝒫 A := fun _ => mem_preimage.mp
/-! ## Cartesian Product -/
/--
For any `Set` `A`, `∅ × A = ∅`.
-/
theorem prod_left_emptyset_eq_emptyset {A : Set α}
: Set.prod (∅ : Set β) A = ∅ := by
unfold prod
simp only [mem_empty_iff_false, false_and, setOf_false]
/--
For any `Set` `A`, `A × ∅ = ∅`.
-/
theorem prod_right_emptyset_eq_emptyset {A : Set α}
: Set.prod A (∅ : Set β) = ∅ := by
unfold prod
simp only [mem_empty_iff_false, and_false, setOf_false]
/--
For any `Set`s `A` and `B`, if both `A` and `B` are nonempty, then `A × B` is
also nonempty.
-/
theorem prod_nonempty_nonempty_imp_nonempty_prod {A : Set α} {B : Set β}
: A ≠ ∅ ∧ B ≠ ∅ ↔ Set.prod A B ≠ ∅ := by
apply Iff.intro
· intro nAB h
have ⟨a, ha⟩ := nonempty_iff_ne_empty.mpr nAB.left
have ⟨b, hb⟩ := nonempty_iff_ne_empty.mpr nAB.right
rw [Set.ext_iff] at h
exact (h (a, b)).mp ⟨ha, hb⟩
· intro h
rw [← nonempty_iff_ne_empty] at h
have ⟨(a, b), ⟨ha, hb⟩⟩ := h
rw [← nonempty_iff_ne_empty, ← nonempty_iff_ne_empty]
exact ⟨⟨a, ha⟩, ⟨b, hb⟩⟩
/-! ## Difference -/
/--
For any sets `A ⊂ B`, if `x ∈ A` then `A - {x} ⊂ B - {x}`.
-/
theorem diff_ssubset_diff_left {A B : Set α} (h : A ⊂ B)
: x ∈ A → A \ {x} ⊂ B \ {x} := by
intro hx
rw [Set.ssubset_def]
apply And.intro
· exact diff_subset_diff_left (subset_of_ssubset h)
· by_contra nh
have : {x} ⊆ A := singleton_subset_iff.mpr hx
rw [diff_subset_iff, union_diff_cancel this] at nh
exact LT.lt.false (Set.ssubset_of_ssubset_of_subset h nh)
/--
For any sets `A ⊂ B`, `B \ A` is nonempty.
-/
theorem diff_ssubset_nonempty {A B : Set α} (h : A ⊂ B)
: Set.Nonempty (B \ A) := by
have : B = A (B \ A) := by
simp only [Set.union_diff_self]
exact (Set.left_subset_union_eq_self (subset_of_ssubset h)).symm
rw [this, Set.ssubset_def] at h
have : ¬ ∀ x, x ∈ A (B \ A) → x ∈ A := h.right
simp only [Set.mem_union, not_forall, exists_prop] at this
have ⟨x, hx⟩ := this
apply Or.elim hx.left
· intro nx
exact absurd nx hx.right
· intro hx
exact ⟨x, hx⟩
/--
If an element `x` is not a member of a set `A`, then `A - {x} = A`.
-/
theorem not_mem_diff_eq_self {A : Set α} (h : a ∉ A)
: A \ {a} = A := by
ext x
apply Iff.intro
· exact And.left
· intro hx
refine ⟨hx, ?_⟩
simp only [mem_singleton_iff]
by_contra nx
rw [nx] at hx
exact absurd hx h
/--
Given two sets `A` and `B`, `(A - {a}) - (B - {b}) = (A - B) - {a}`.
-/
theorem diff_mem_diff_mem_eq_diff_diff_mem {A B : Set α} {a : α}
: (A \ {a}) \ (B \ {a}) = (A \ B) \ {a} := by
calc (A \ {a}) \ (B \ {a})
_ = { x | x ∈ A \ {a} ∧ x ∉ B \ {a} } := rfl
_ = { x | x ∈ A \ {a} ∧ ¬(x ∈ B \ {a}) } := rfl
_ = { x | (x ∈ A ∧ x ≠ a) ∧ ¬(x ∈ B ∧ x ≠ a) } := rfl
_ = { x | (x ∈ A ∧ x ≠ a) ∧ (x ∉ B x = a) } := by
ext x
rw [mem_setOf_eq, not_and_de_morgan]
simp
_ = { x | (x ∈ A ∧ x ≠ a ∧ x ∉ B) (x ∈ A ∧ x ≠ a ∧ x = a) } := by
ext x
simp only [mem_setOf_eq]
rw [and_or_left, and_assoc, and_assoc]
_ = { x | x ∈ A ∧ x ≠ a ∧ x ∉ B } := by simp
_ = { x | x ∈ A ∧ x ∉ B ∧ x ≠ a } := by
ext x
simp only [ne_eq, sep_and, mem_inter_iff, mem_setOf_eq]
apply Iff.intro <;>
· intro ⟨⟨_, hx₂⟩, hx₃, hx₄⟩
exact ⟨⟨hx₃, hx₄⟩, ⟨hx₃, hx₂⟩⟩
_ = { x | x ∈ A ∧ x ∉ B ∧ x ∉ ({a} : Set α) } := rfl
_ = { x | x ∈ A \ B ∧ x ∉ ({a} : Set α) } := by
ext x
simp only [
mem_singleton_iff,
sep_and,
mem_inter_iff,
mem_setOf_eq,
mem_diff,
and_congr_right_iff,
and_iff_right_iff_imp,
and_imp
]
intro hx _ _
exact hx
_ = (A \ B) \ {a} := rfl
/--
For any set `A`, the difference between the sample space and `A` is the
complement of `A`.
-/
theorem univ_diff_self_eq_compl (A : Set α) : Set.univ \ A = A.compl := by
unfold Set.compl SDiff.sdiff instSDiffSet Set.diff
simp only [mem_univ, true_and]
/--
For any set `A`, the difference between the sample space and the complement of
`A` is `A`.
-/
theorem univ_diff_compl_eq_self (A : Set α) : Set.univ \ A.compl = A := by
unfold Set.compl SDiff.sdiff instSDiffSet Set.diff
simp only [mem_univ, mem_setOf_eq, not_not, true_and, setOf_mem_eq]
/-! ## Symmetric Difference -/
/--
If `x ∈ A` and `x ∉ B`, then `x ∈ A ∆ B`.
-/
theorem symm_diff_mem_left {A B : Set α} (hA : x ∈ A) (hB : x ∉ B)
: x ∈ A ∆ B := by
left
exact ⟨hA, hB⟩
/--
If `x ∉ A` and `x ∈ B`, then `x ∈ A ∆ B`.
-/
theorem symm_diff_mem_right {A B : Set α} (hA : x ∉ A) (hB : x ∈ B)
: x ∈ A ∆ B := by
right
exact ⟨hB, hA⟩
/--
If `x ∈ A` and `x ∈ B`, then `x ∉ A ∆ B`.
-/
theorem symm_diff_mem_both_not_mem {A B : Set α} (hA : x ∈ A) (hB : x ∈ B)
: x ∉ A ∆ B := by
intro h
apply Or.elim h
· intro ⟨_, nB⟩
exact absurd hB nB
· intro ⟨_, nA⟩
exact absurd hA nA
/--
If `x ∉ A` and `x ∉ B`, then `x ∉ A ∆ B`.
-/
theorem symm_diff_not_mem_both_not_mem {A B : Set α} (nA : x ∉ A) (nB : x ∉ B)
: x ∉ A ∆ B := by
intro h
apply Or.elim h
· intro ⟨hA, _⟩
exact absurd hA nA
· intro ⟨hB, _⟩
exact absurd hB nB
/--
`x` is a member of the `symmDiff` of `A` and `B` **iff** `x ∈ A ∧ x ∉ B` or
`x ∉ A ∧ x ∈ B`.
-/
theorem mem_symm_diff_iff_exclusive_mem {A B : Set α}
: x ∈ (A ∆ B) ↔ (x ∈ A ∧ x ∉ B) (x ∉ A ∧ x ∈ B) := by
unfold symmDiff
apply Iff.intro
· intro hx
simp at hx
conv => arg 2; rw [and_comm]
exact hx
· intro hx
simp
conv => arg 2; rw [and_comm]
exact hx
/--
`x` is not a member of the `symmDiff` of `A` and `B` **iff** `x ∈ A ∩ B` or
`x ∉ A B`.
This is the contraposition of `mem_symm_diff_iff_exclusive_mem`.
-/
theorem not_mem_symm_diff_inter_or_not_union {A B : Set α}
: x ∉ (A ∆ B) ↔ (x ∈ A ∩ B) (x ∉ A B) := by
show ¬(x ∈ A ∧ ¬x ∈ B x ∈ B ∧ ¬x ∈ A) ↔ x ∈ A ∧ x ∈ B ¬(x ∈ A x ∈ B)
rw [
not_or_de_morgan,
not_and_de_morgan, not_and_de_morgan,
not_not, not_not,
not_or_de_morgan
]
apply Iff.intro
· intro nx
apply Or.elim nx.left
· intro nA
exact Or.elim nx.right (Or.inr ⟨nA, ·⟩) (absurd · nA)
· intro hB
exact Or.elim nx.right (absurd hB ·) (Or.inl ⟨·, hB⟩)
· intro hx
apply Or.elim hx
· intro hy
exact ⟨Or.inr hy.right, Or.inr hy.left⟩
· intro hy
exact ⟨Or.inl hy.left, Or.inl hy.right⟩
end Set