2023-05-18 20:04:20 +00:00
|
|
|
|
import Mathlib.Init.Set
|
2023-05-18 22:02:15 +00:00
|
|
|
|
import Mathlib.Data.Set.Basic
|
|
|
|
|
import Mathlib.Tactic.LibrarySearch
|
2023-05-18 20:04:20 +00:00
|
|
|
|
|
|
|
|
|
/-! # Enderton.Chapter_1
|
|
|
|
|
|
|
|
|
|
Introduction
|
|
|
|
|
-/
|
|
|
|
|
|
|
|
|
|
namespace Enderton.Set.Chapter_1
|
|
|
|
|
|
2023-05-19 15:25:37 +00:00
|
|
|
|
/-! ### Exercise 1.1
|
2023-05-18 20:04:20 +00:00
|
|
|
|
|
2023-05-18 22:02:15 +00:00
|
|
|
|
Which of the following become true when "∈" is inserted in place of the blank?
|
|
|
|
|
Which become true when "⊆" is inserted?
|
|
|
|
|
-/
|
|
|
|
|
|
|
|
|
|
/--
|
|
|
|
|
The `∅` does not equal the singleton set containing `∅`.
|
|
|
|
|
-/
|
|
|
|
|
lemma empty_ne_singleton_empty (h : ∅ = ({∅} : Set (Set α))) : False :=
|
|
|
|
|
absurd h (Ne.symm $ Set.singleton_ne_empty (∅ : Set α))
|
|
|
|
|
|
2023-05-19 15:25:37 +00:00
|
|
|
|
/-- #### Exercise 1.1a
|
2023-05-18 22:02:15 +00:00
|
|
|
|
|
|
|
|
|
`{∅} ___ {∅, {∅}}`
|
|
|
|
|
-/
|
2023-05-19 15:25:37 +00:00
|
|
|
|
theorem exercise_1_1a
|
2023-05-18 22:02:15 +00:00
|
|
|
|
: {∅} ∈ ({∅, {∅}} : Set (Set (Set α)))
|
|
|
|
|
∧ {∅} ⊆ ({∅, {∅}} : Set (Set (Set α))) := ⟨by simp, by simp⟩
|
|
|
|
|
|
2023-05-19 15:25:37 +00:00
|
|
|
|
/-- #### Exercise 1.1b
|
2023-05-18 22:02:15 +00:00
|
|
|
|
|
|
|
|
|
`{∅} ___ {∅, {{∅}}}`
|
|
|
|
|
-/
|
2023-05-19 15:25:37 +00:00
|
|
|
|
theorem exercise_1_1b
|
2023-05-18 22:02:15 +00:00
|
|
|
|
: {∅} ∉ ({∅, {{∅}}}: Set (Set (Set (Set α))))
|
|
|
|
|
∧ {∅} ⊆ ({∅, {{∅}}}: Set (Set (Set (Set α)))) := by
|
|
|
|
|
refine ⟨?_, by simp⟩
|
|
|
|
|
intro h
|
|
|
|
|
simp at h
|
|
|
|
|
exact empty_ne_singleton_empty h
|
|
|
|
|
|
2023-05-19 15:25:37 +00:00
|
|
|
|
/-- #### Exercise 1.1c
|
2023-05-18 22:02:15 +00:00
|
|
|
|
|
|
|
|
|
`{{∅}} ___ {∅, {∅}}`
|
|
|
|
|
-/
|
2023-05-19 15:25:37 +00:00
|
|
|
|
theorem exercise_1_1c
|
2023-05-18 22:02:15 +00:00
|
|
|
|
: {{∅}} ∉ ({∅, {∅}} : Set (Set (Set (Set α))))
|
|
|
|
|
∧ {{∅}} ⊆ ({∅, {∅}} : Set (Set (Set (Set α)))) := ⟨by simp, by simp⟩
|
|
|
|
|
|
2023-05-19 15:25:37 +00:00
|
|
|
|
/-- #### Exercise 1.1d
|
2023-05-18 20:04:20 +00:00
|
|
|
|
|
2023-05-18 22:02:15 +00:00
|
|
|
|
`{{∅}} ___ {∅, {{∅}}}`
|
|
|
|
|
-/
|
2023-05-19 15:25:37 +00:00
|
|
|
|
theorem exercise_1_1d
|
2023-05-18 22:02:15 +00:00
|
|
|
|
: {{∅}} ∈ ({∅, {{∅}}} : Set (Set (Set (Set α))))
|
|
|
|
|
∧ ¬ {{∅}} ⊆ ({∅, {{∅}}} : Set (Set (Set (Set α)))) := by
|
|
|
|
|
refine ⟨by simp, ?_⟩
|
|
|
|
|
intro h
|
|
|
|
|
simp at h
|
|
|
|
|
exact empty_ne_singleton_empty h
|
|
|
|
|
|
2023-05-19 15:25:37 +00:00
|
|
|
|
/-- #### Exercise 1.1e
|
2023-05-18 22:02:15 +00:00
|
|
|
|
|
|
|
|
|
`{{∅}} ___ {∅, {∅, {∅}}}`
|
|
|
|
|
-/
|
2023-05-19 15:25:37 +00:00
|
|
|
|
theorem exercise_1_1e
|
2023-05-18 22:02:15 +00:00
|
|
|
|
: {{∅}} ∉ ({∅, {∅, {∅}}} : Set (Set (Set (Set α))))
|
|
|
|
|
∧ ¬ {{∅}} ⊆ ({∅, {∅, {∅}}} : Set (Set (Set (Set α)))) := by
|
|
|
|
|
apply And.intro
|
|
|
|
|
· intro h
|
|
|
|
|
simp at h
|
|
|
|
|
rw [Set.ext_iff] at h
|
|
|
|
|
have nh := h ∅
|
|
|
|
|
simp at nh
|
|
|
|
|
exact empty_ne_singleton_empty nh
|
|
|
|
|
· intro h
|
|
|
|
|
simp at h
|
|
|
|
|
rw [Set.ext_iff] at h
|
|
|
|
|
have nh := h {∅}
|
|
|
|
|
simp at nh
|
|
|
|
|
|
2023-05-19 15:25:37 +00:00
|
|
|
|
/-- ### Exercise 1.2
|
2023-05-18 22:02:15 +00:00
|
|
|
|
|
|
|
|
|
Show that no two of the three sets `∅`, `{∅}`, and `{{∅}}` are equal to each
|
|
|
|
|
other.
|
|
|
|
|
-/
|
2023-05-19 15:25:37 +00:00
|
|
|
|
theorem exercise_1_2
|
2023-05-18 22:02:15 +00:00
|
|
|
|
: ∅ ≠ ({∅} : Set (Set α))
|
|
|
|
|
∧ ∅ ≠ ({{∅}} : Set (Set (Set α)))
|
|
|
|
|
∧ {∅} ≠ ({{∅}} : Set (Set (Set α))) := by
|
|
|
|
|
refine ⟨?_, ⟨?_, ?_⟩⟩
|
|
|
|
|
· intro h
|
|
|
|
|
exact empty_ne_singleton_empty h
|
|
|
|
|
· intro h
|
|
|
|
|
exact absurd h (Ne.symm $ Set.singleton_ne_empty ({∅} : Set (Set α)))
|
|
|
|
|
· intro h
|
|
|
|
|
simp at h
|
|
|
|
|
exact empty_ne_singleton_empty h
|
|
|
|
|
|
2023-05-19 15:25:37 +00:00
|
|
|
|
/-- ### Exercise 1.3
|
2023-05-18 22:02:15 +00:00
|
|
|
|
|
|
|
|
|
Show that if `B ⊆ C`, then `𝓟 B ⊆ 𝓟 C`.
|
|
|
|
|
-/
|
2023-05-19 15:25:37 +00:00
|
|
|
|
theorem exercise_1_3 (h : B ⊆ C) : Set.powerset B ⊆ Set.powerset C := by
|
2023-05-18 22:02:15 +00:00
|
|
|
|
unfold Set.powerset
|
|
|
|
|
simp
|
|
|
|
|
intro x hx
|
|
|
|
|
exact Set.Subset.trans hx h
|
|
|
|
|
|
2023-05-19 15:25:37 +00:00
|
|
|
|
/-- ### Exercise 1.4
|
2023-05-18 22:02:15 +00:00
|
|
|
|
|
|
|
|
|
Assume that `x` and `y` are members of a set `B`. Show that
|
|
|
|
|
`{{x}, {x, y}} ∈ 𝓟 𝓟 B`.
|
|
|
|
|
-/
|
2023-05-19 15:25:37 +00:00
|
|
|
|
theorem exercise_1_4 (x y : α) (hx : x ∈ B) (hy : y ∈ B)
|
2023-05-18 22:02:15 +00:00
|
|
|
|
: {{x}, {x, y}} ∈ Set.powerset (Set.powerset B) := by
|
|
|
|
|
unfold Set.powerset
|
|
|
|
|
simp only [Set.mem_singleton_iff, Set.mem_setOf_eq]
|
|
|
|
|
rw [Set.subset_def]
|
|
|
|
|
intro z hz
|
|
|
|
|
simp at hz
|
|
|
|
|
apply Or.elim hz
|
|
|
|
|
· intro h
|
|
|
|
|
rwa [h, Set.mem_setOf_eq, Set.singleton_subset_iff]
|
|
|
|
|
· intro h
|
|
|
|
|
rw [h, Set.mem_setOf_eq]
|
|
|
|
|
exact Set.union_subset
|
|
|
|
|
(Set.singleton_subset_iff.mpr hx)
|
|
|
|
|
(Set.singleton_subset_iff.mpr hy)
|
2023-05-18 20:04:20 +00:00
|
|
|
|
|
|
|
|
|
end Enderton.Set.Chapter_1
|