My solutions to Tao's Analysis I, formalized in Lean
Add equality lemma for mk_cartesian
authored by
GitHub
bec70168
49a11de7
+5
+5
analysis/Analysis/Section_3_5.lean
+5
analysis/Analysis/Section_3_5.lean
···
119
119
obtain ⟨ x', hx: z.val = (⟨ x', snd z ⟩:OrderedPair) ⟩ := (exists_comm.mp this).choose_spec
120
120
simp [z, mk_cartesian, Subtype.val_inj] at hx ⊢; rw [←hx.2]
121
121
122
+
@[simp]
123
+
theorem SetTheory.Set.mk_cartesian_eq {X Y: Set} (z: X ×ˢ Y) :
124
+
(mk_cartesian (fst z) (snd z)) = z := by
125
+
rw [mk_cartesian, Subtype.mk.injEq, pair_eq_fst_snd]
126
+
122
127
noncomputable abbrev SetTheory.Set.uncurry {X Y Z:Set} (f: X → Y → Z) : X ×ˢ Y → Z :=
123
128
fun z ↦ f (fst z) (snd z)
124
129