Quotients for sets

ZFLean/Def.lean

@@ -120,6 +120,13 @@ private lemma some_inf_mem_sep_inductive_set : some_inf ∈ some_inf.powerset.se
   simp only [mem_sep, mem_powerset, subset_refl, true_and]
   exact inductive_some_inf
 
+theorem sdiff_subset {s t : ZFSet} : s \ t ⊆ s := by
+  intro x
+  rw [mem_sdiff]
+  rintro ⟨h, _⟩
+  exact h
+
+/-- Symmetric difference of two sets, denoted by `Δ`. -/
 def symmDiff (p q : ZFSet) : ZFSet := (p \ q) ∪ (q \ p)
 infix:70 " Δ " => symmDiff
 
@@ -163,6 +170,80 @@ theorem inter_mono {x y z : ZFSet} :  x ⊆ z → y ⊆ z → x ∩ y ⊆ z := b
   rw [ZFSet.mem_inter] at ha
   exact hx ha.1
 
+
+theorem non_empty_pair {a b : ZFSet} : Nonempty (a.pair b) := by
+  rw [pair]
+  exact ⟨{a}, mem_insert {a} {{a, b}}⟩
+
+def π₁ (x : ZFSet) : ZFSet := ⋃₀ (⋂₀ x)
+
+open Classical in -- couldn't find another way
+noncomputable def π₂ (x : ZFSet) : ZFSet :=
+  let δ : ZFSet := (⋃₀ x \ ⋂₀ x)
+  if δ = ∅ then π₁ x else ⋃₀ δ
+
+@[simp] theorem π₁_pair (x y : ZFSet) : π₁ (x.pair y) = x := by
+  unfold π₁ pair
+  ext
+  rw [sInter_pair, mem_sUnion]
+  constructor
+  · rintro ⟨w, l, r⟩
+    rw [mem_inter, mem_singleton, mem_pair] at l
+    rw [l.1] at r
+    assumption
+  · intro h
+    exists x
+    rw [mem_inter, mem_singleton, mem_pair]
+    exact ⟨⟨rfl, .inl rfl⟩, h⟩
+
+@[simp] theorem pair_inter {x y : ZFSet} : {x} ∩ {x, y} = ({x} : ZFSet) := by
+    ext
+    rw [mem_inter, mem_singleton, mem_pair]
+    constructor
+    · rintro ⟨rfl, _ | rfl⟩ <;> rfl
+    · rintro rfl
+      exact ⟨rfl, .inl rfl⟩
+
+@[simp] theorem pair_union {x y : ZFSet} : {x} ∪ {x, y} = ({x, y} : ZFSet) := by
+    ext
+    rw [mem_union, mem_singleton, mem_pair]
+    exact or_self_left
+
+@[simp] theorem pair_minus {x y : ZFSet} : x ≠ y → {x, y} \ {x} = ({y} : ZFSet) := by
+  intro x_ne_y
+  ext z
+  rw [mem_sdiff, mem_pair, mem_singleton, mem_singleton]
+  constructor
+  · rintro ⟨rfl | rfl, r⟩
+    · contradiction
+    · rfl
+  · rintro rfl
+    exact ⟨.inr rfl, x_ne_y ∘ Eq.symm⟩
+
+@[simp] theorem π₂_pair (x y : ZFSet) : π₂ (x.pair y) = y := by
+  unfold π₂
+  dsimp
+  split_ifs with h
+  · rw [π₁_pair]
+    unfold pair at h
+    rw [sUnion_pair, pair_union, sInter_pair, pair_inter] at h
+    rw [ZFSet.ext_iff] at h
+    specialize h y
+    simpa only [mem_sdiff, mem_insert_iff, mem_singleton, eq_self,
+      or_true, true_and, notMem_empty, iff_false, not_not, eq_comm] using h
+  · unfold pair at *
+    rw [sUnion_pair, pair_union, sInter_pair, pair_inter] at h ⊢
+    rw [pair_minus]
+    · exact sUnion_singleton
+    · intro h'
+      rw [h'] at h
+      simp [ZFSet.ext_iff] at h
+
+theorem pair_eta {z A B : ZFSet} (h : z ∈ A.prod B) : z = z.π₁.pair z.π₂ := by
+  rw [mem_prod] at h
+  obtain ⟨a, ha, b, hb, rfl⟩ := h
+  rw [π₁_pair, π₂_pair]
+
 end Preamble
 
 end ZFSet