feat : Real numbers, Field and OrderedRing

ZFLean/Functions.lean

@@ -1204,16 +1204,22 @@ theorem mem_funs_of_lambda {A B : ZFSet} {f : ZFSet → ZFSet} (hf : ∀ {x}, x
 attribute [zfun] lambda_isFunc
 attribute [zrel] lambda_subset
 
-theorem fapply_lambda {A B : ZFSet} {f : ZFSet → ZFSet}
+theorem fapply_lambda' {A B : ZFSet} {f : ZFSet → ZFSet}
   (hf : ∀ {x}, x ∈ A → f x ∈ B) {a : ZFSet} (ha : a ∈ A) :
     fapply (λᶻ : A → B | x ↦ f x) (is_func_is_pfunc <| lambda_isFunc hf)
-      ⟨a, by zdom⟩ = f a := by
+      ⟨a, by zdom⟩ = ⟨f a, hf ha⟩ := by
   rw [fapply]
   generalize_proofs choose_y y_mem_B
   have y_def := Classical.choose_spec choose_y |>.2
   rw [lambda_spec] at y_def
+  apply Subtype.ext
   exact y_def.2.2
 
+theorem fapply_lambda {A B : ZFSet} {f : ZFSet → ZFSet}
+  (hf : ∀ {x}, x ∈ A → f x ∈ B) {a : ZFSet} (ha : a ∈ A) :
+    fapply (λᶻ : A → B | x ↦ f x) (is_func_is_pfunc <| lambda_isFunc hf)
+      ⟨a, by zdom⟩ = f a := Subtype.ext_iff.mp <| fapply_lambda' hf ha
+
 /--
 The inverse of an injection is a function.
 -/

ZFLean/Naturals.lean

@@ -1676,6 +1676,31 @@ instance : TransferEquiv ZFNat ℕ := ⟨ringEquivNat.toEquiv⟩
 
 @[transfer_simps] theorem ringEquivNat_lt (a b : ZFNat) :
     a < b ↔ ringEquivNat a < ringEquivNat b := toNat_lt a b
+
+@[transfer_simps] theorem ringEquivNat_max (a b : ZFNat) :
+    ringEquivNat (max a b) = max (ringEquivNat a) (ringEquivNat b) := by
+  rw [eq_comm, max_eq_iff]
+  rcases le_or_gt a b with h | h
+  · apply Or.inr
+    rw [max_eq_right h, ← ringEquivNat_le]
+    exact ⟨rfl, h⟩
+  · apply Or.inl
+    apply le_of_lt at h
+    rw [max_eq_left h, ← ringEquivNat_le]
+    exact ⟨rfl, h⟩
+
+@[transfer_simps] theorem ringEquivNat_min (a b : ZFNat) :
+    ringEquivNat (min a b) = min (ringEquivNat a) (ringEquivNat b) := by
+  rw [eq_comm, min_eq_iff]
+  rcases le_or_gt a b with h | h
+  · apply Or.inl
+    rw [min_eq_left h, ← ringEquivNat_le]
+    exact ⟨rfl, h⟩
+  · apply Or.inr
+    apply le_of_lt at h
+    rw [min_eq_right h, ← ringEquivNat_le]
+    exact ⟨rfl, h⟩
+
 end ZFNat
 
 end Transfer

ZFLean/Quotient.lean

@@ -223,6 +223,71 @@ theorem lift_class_of (hrR : R ⊆ E.prod E := by zrel)
   rw [of_in_class, ←mem_class_of_iff_related hrR heR]
   exact Subtype.prop <| choose_repr <| class_of _ _ x
 
+noncomputable def lift₂ (f : E → E → α) (C D : E.ZFQuotient R) : α :=
+  (f (of_in_class (choose_repr C)) (of_in_class (choose_repr D)))
+
+theorem lift₂_class_of (hrR : R ⊆ E.prod E := by zrel)
+  (heR : R.is_rel_equivalence hrR := by assumption) (f : E → E → α)
+  (h : ∀ a b c d, a.val.pair b.val ∈ R → c.val.pair d.val ∈ R → f a c = f b d) (x y : E) :
+    lift₂ f (class_of hrR heR x) (class_of hrR heR y) = f x y := by
+  apply h <;> rw [of_in_class, ←mem_class_of_iff_related hrR heR]
+  · exact Subtype.prop <| choose_repr <| class_of _ _ x
+  · exact Subtype.prop <| choose_repr <| class_of _ _ y
+
+noncomputable def map (hrR : R ⊆ E.prod E := by zrel)
+  (heR : R.is_rel_equivalence hrR := by assumption) (f : E → E)
+  (h : ∀ a b, a.val.pair b.val ∈ R → (f a).val.pair (f b).val ∈ R) :
+    E.ZFQuotient R → E.ZFQuotient R :=
+  fun C => ⟨lift (fun r => class_of hrR heR (f r)) C, by
+    have r := choose_repr C
+    rw [←class_of_mem_eq_self hrR heR C r, lift_class_of]
+    · exact (class_of hrR heR (f (of_in_class r))).prop
+    · intro a b related
+      rw [←Subtype.ext_iff, class_eq_iff_related]
+      exact h a b related
+  ⟩
+
+theorem map_class_of (hrR : R ⊆ E.prod E := by zrel)
+(heR : R.is_rel_equivalence hrR := by assumption) (f : E → E)
+(h : ∀ a b, a.val.pair b.val ∈ R → (f a).val.pair (f b).val ∈ R) (x : E) :
+    map hrR heR f h (class_of hrR heR x) = class_of hrR heR (f x) := by
+  unfold map
+  conv =>
+    enter [1,1]
+    rw [lift_class_of hrR heR] ; · skip
+    tactic =>
+      intro a b related
+      rw [←Subtype.ext_iff, class_eq_iff_related]
+      exact h a b related
+
+noncomputable def map₂ (hrR : R ⊆ E.prod E := by zrel)
+  (heR : R.is_rel_equivalence hrR := by assumption) (f : E → E → E)
+  (h : ∀ a b c d, a.val.pair b.val ∈ R → c.val.pair d.val ∈ R → (f a c).val.pair (f b d) ∈ R) :
+    E.ZFQuotient R → E.ZFQuotient R → E.ZFQuotient R :=
+  fun C D => ⟨lift₂ (fun r s => class_of hrR heR (f r s)) C D, by
+    have r := choose_repr C
+    have s := choose_repr D
+    rw [←class_of_mem_eq_self hrR heR C r, ←class_of_mem_eq_self hrR heR D s, lift₂_class_of]
+    · exact (class_of hrR heR (f (of_in_class r) (of_in_class s))).prop
+    · intro a b c d ab_related cd_related
+      rw [←Subtype.ext_iff, class_eq_iff_related]
+      exact h a b c d ab_related cd_related
+  ⟩
+
+theorem map₂_class_of (hrR : R ⊆ E.prod E := by zrel)
+  (heR : R.is_rel_equivalence hrR := by assumption) (f : E → E → E)
+  (h : ∀ a b c d, a.val.pair b.val ∈ R → c.val.pair d.val ∈ R → (f a c).val.pair (f b d) ∈ R)
+  (x y : E) :
+    map₂ hrR heR f h (class_of hrR heR x) (class_of hrR heR y) = class_of hrR heR (f x y) := by
+  unfold map₂
+  conv =>
+    enter [1,1]
+    rw [lift₂_class_of hrR heR] ; · skip
+    tactic =>
+      intro a b c d ab_related cd_related
+      rw [←Subtype.ext_iff, class_eq_iff_related]
+      exact h a b c d ab_related cd_related
+
 @[expose]
 def toSetoid {E R : ZFSet}
     (hrR : R ⊆ E.prod E := by zrel)

ZFLean/Rationals.lean

@@ -880,13 +880,52 @@ theorem equivRat_le (a b : ZFRat) : equivRat a ≤ equivRat b ↔ a ≤ b := by
 theorem equivRat_lt (a b : ZFRat) : equivRat a < equivRat b ↔ a < b := by
   rw [lt_iff_not_ge, lt_iff_not_ge, equivRat_le]
 
+theorem equivRat_abs (a : ZFRat) : |equivRat a| = equivRat |a| :=  by
+  rw [abs_eq_max_neg, abs_eq_max_neg]
+  cases max_cases a (-a) with
+  | inl h =>
+    rw [h.left, max_eq_left]
+    rw [←equivRat.map_neg, equivRat_le]
+    exact h.right
+  | inr h =>
+    rw [h.left, max_eq_right, ←equivRat.map_neg]
+    rw [←equivRat.map_neg, equivRat_le]
+    apply le_of_lt
+    exact h.right
+
 /-- Equivalence used by the `transfer` tactic to move goals between `ZFRat` and `ℚ`. -/
 noncomputable instance : TransferEquiv ZFRat ℚ := ⟨equivRat.toEquiv⟩
 
-attribute [transfer_simps ←] equivRat_le equivRat_lt
+attribute [transfer_simps ←] equivRat_le equivRat_lt equivRat_abs
 
 end Transfer
 
+section Analysis
+
+theorem abs_inv (a : ZFRat) : |a⁻¹| = |a|⁻¹ := by
+  rcases lt_trichotomy a 0 with h | rfl | h
+  · rw [abs_of_neg <| inv_neg''.mpr h, abs_of_neg h, inv_neg]
+  · rw [inv_zero, abs_zero, inv_zero]
+  · rw [abs_of_pos <| inv_pos.mpr h, abs_of_pos h]
+
+theorem separation (a : ZFRat) : a = 0 ↔ ∀ e : ZFRat, 0 < e → |a| < e := by
+  constructor
+  · intro rfl e ep
+    rw [abs_zero]
+    exact ep
+  · intro h
+    by_contra
+    rw [←ne_eq, ←abs_pos] at this
+    absurd h (|a|/2) (div_pos this two_pos)
+    rw [not_lt, Field.div_eq_mul_inv]
+    conv => right ; rw [←mul_one |a|]
+    rw [mul_le_mul_iff_of_pos_left this]
+    apply inv_le_of_inv_le₀ one_pos
+    rw [inv_one, ←one_add_one_eq_two, le_add_iff_nonneg_left]
+    exact zero_le_one
+
+end Analysis
+
 end ZFRat
 
 /- The carrier set of Rat, which is equivalent to the carrier type of ZFRat -/