From 982ee74602514eeb221548944e9c124e875e6529 Mon Sep 17 00:00:00 2001 From: palalansouki Date: Sun, 5 Oct 2025 16:25:26 +0900 Subject: [PATCH 1/3] two_pow_cardEQ_power --- Foundation/FirstOrder/Z/Basic.lean | 66 ++++++++----- Foundation/FirstOrder/Z/Function.lean | 128 ++++++++++++++++++++++++-- 2 files changed, 160 insertions(+), 34 deletions(-) diff --git a/Foundation/FirstOrder/Z/Basic.lean b/Foundation/FirstOrder/Z/Basic.lean index 7b867ed1..5ed62e1f 100644 --- a/Foundation/FirstOrder/Z/Basic.lean +++ b/Foundation/FirstOrder/Z/Basic.lean @@ -274,42 +274,42 @@ lemma union_assoc (x y z : V) : (x ∪ y) ∪ z = x ∪ (y ∪ z) := by ext; sim /-! ### Insert -/ -noncomputable def insert (x y : V) : V := {x} ∪ y +protected noncomputable def insert (x y : V) : V := {x} ∪ y -noncomputable scoped instance : Insert V V := ⟨insert⟩ +noncomputable scoped instance : Insert V V := ⟨Zermelo.insert⟩ -lemma insert_def (x y : V) : Insert.insert x y = {x} ∪ y := rfl +lemma insert_def (x y : V) : insert x y = {x} ∪ y := rfl def insert.dfn : Semisentence ℒₛₑₜ 3 := “u x y. ∀ s, !singleton.dfn s x → !union.dfn u s y” -instance insert.defined : ℒₛₑₜ-function₂[V] Insert.insert via insert.dfn := +instance insert.defined : ℒₛₑₜ-function₂[V] insert via insert.dfn := ⟨by intro v; simp [insert.dfn, insert_def]⟩ -instance insert.definable : ℒₛₑₜ-function₂[V] Insert.insert := insert.defined.to_definable +instance insert.definable : ℒₛₑₜ-function₂[V] insert := insert.defined.to_definable -@[simp] lemma mem_insert {x y z : V} : z ∈ Insert.insert x y ↔ z = x ∨ z ∈ y := by simp [insert_def] +@[simp] lemma mem_insert {x y z : V} : z ∈ insert x y ↔ z = x ∨ z ∈ y := by simp [insert_def] -@[simp] lemma insert_empty_eq (x : V) : (Insert.insert x ∅ : V) = {x} := by ext; simp +@[simp] lemma insert_empty_eq (x : V) : (insert x ∅ : V) = {x} := by ext; simp -lemma union_insert (x y : V) : x ∪ Insert.insert y z = Insert.insert y (x ∪ z) := by ext; simp; tauto +lemma union_insert (x y : V) : x ∪ insert y z = insert y (x ∪ z) := by ext; simp; tauto lemma pair_eq_doubleton (x y : V) : {x, y} = doubleton x y := by ext; simp -@[simp] lemma sUnion_insert (x y : V) : ⋃ˢ Insert.insert x y = x ∪ ⋃ˢ y := by ext; simp [mem_sUnion_iff] +@[simp] lemma sUnion_insert (x y : V) : ⋃ˢ insert x y = x ∪ ⋃ˢ y := by ext; simp [mem_sUnion_iff] -@[simp] lemma subset_insert (x y : V) : y ⊆ Insert.insert x y := by simp [insert_def] +@[simp] lemma subset_insert (x y : V) : y ⊆ insert x y := by simp [insert_def] -@[simp] instance insert_isNonempty (x y : V) : IsNonempty (Insert.insert x y) := ⟨x, by simp⟩ +@[simp] instance insert_isNonempty (x y : V) : IsNonempty (insert x y) := ⟨x, by simp⟩ @[simp] lemma intsert_union (x y z : V) : - Insert.insert x y ∪ z = Insert.insert x (y ∪ z) := by + insert x y ∪ z = insert x (y ∪ z) := by ext; simp only [mem_union_iff, mem_insert]; grind @[simp] lemma singleton_inter (x y : V) : - {x} ∪ y = Insert.insert x y := by + {x} ∪ y = insert x y := by ext; simp -@[simp, grind] lemma insert_eq_self_of_mem {x y : V} (hx : x ∈ y) : Insert.insert x y = y := by +@[simp, grind] lemma insert_eq_self_of_mem {x y : V} (hx : x ∈ y) : insert x y = y := by ext; simp only [mem_insert, or_iff_right_iff_imp]; grind /-! ## Axiom of power set -/ @@ -462,15 +462,15 @@ lemma inter_assoc (x y z : V) : (x ∩ y) ∩ z = x ∩ (y ∩ z) := by ext; sim @[simp] lemma empty_inter (x : V) : ∅ ∩ x = ∅ := by ext; simp -@[simp] lemma sInter_insert (x y : V) [hy : IsNonempty y] : ⋂ˢ Insert.insert x y = x ∩ ⋂ˢ y := by +@[simp] lemma sInter_insert (x y : V) [hy : IsNonempty y] : ⋂ˢ insert x y = x ∩ ⋂ˢ y := by ext; simp [*, mem_sInter_iff_of_nonempty] @[simp, grind] lemma intsert_inter_of_mem (x y z : V) (hx : x ∈ z) : - Insert.insert x y ∩ z = Insert.insert x (y ∩ z) := by + insert x y ∩ z = insert x (y ∩ z) := by ext; simp only [inter_comm, mem_inter_iff, mem_insert]; grind @[simp, grind] lemma intsert_inter_of_not_mem (x y z : V) (hx : x ∉ z) : - Insert.insert x y ∩ z = y ∩ z := by + insert x y ∩ z = y ∩ z := by ext; simp only [inter_comm, mem_inter_iff, mem_insert]; grind @[simp, grind] lemma singleton_inter_of_mem {x y : V} (hx : x ∈ y) : @@ -515,11 +515,11 @@ instance sdiff.definable : ℒₛₑₜ-function₂[V] SDiff.sdiff := sdiff.defi ext; simp only [mem_sdiff_iff, mem_singleton_iff, and_iff_left_iff_imp]; grind @[simp, grind] lemma insert_sdiff_of_mem {x y z : V} (hx : x ∈ z) : - Insert.insert x y \ z = y \ z := by + insert x y \ z = y \ z := by ext; simp only [mem_sdiff_iff, mem_insert, and_congr_left_iff, or_iff_right_iff_imp]; grind @[simp, grind] lemma insert_sdiff_of_not_mem {x y z : V} (hx : x ∉ z) : - Insert.insert x y \ z = Insert.insert x (y \ z) := by + insert x y \ z = insert x (y \ z) := by ext; simp only [mem_sdiff_iff, mem_insert]; grind lemma isNonempty_sdiff_of_ssubset {x y : V} : x ⊊ y → IsNonempty (y \ x) := by @@ -647,16 +647,16 @@ lemma union_prod (x y z : V) : (x ∪ y) ×ˢ z = (x ×ˢ z) ∪ (y ×ˢ z) := b ext z; simp [mem_prod_iff] lemma insert_kpair_subset_insert_prod_insert_of_subset_prod {R X Y : V} (h : R ⊆ X ×ˢ Y) (x y : V) : - Insert.insert ⟨x, y⟩ₖ R ⊆ Insert.insert x X ×ˢ Insert.insert y Y := by + insert ⟨x, y⟩ₖ R ⊆ insert x X ×ˢ insert y Y := by intro z hz rcases show z = ⟨x, y⟩ₖ ∨ z ∈ R by simpa using hz with (rfl | hz) · simp · exact prod_subset_prod_of_subset - (show X ⊆ Insert.insert x X by simp) (show Y ⊆ Insert.insert y Y by simp) z (h z hz) + (show X ⊆ insert x X by simp) (show Y ⊆ insert y Y by simp) z (h z hz) /-! ## Axiom of infinity -/ -noncomputable def succ (x : V) : V := Insert.insert x x +noncomputable def succ (x : V) : V := insert x x lemma mem_succ_iff {x y : V} : y ∈ succ x ↔ y = x ∨ y ∈ x := by simp [succ] @@ -742,10 +742,28 @@ lemma num_succ_def (n : ℕ) : ((n + 1 : ℕ) : V) = succ ↑n := rfl @[simp] lemma cast_one_def : ((1 : ℕ) : V) = 1 := rfl -lemma one_def : (1 : V) = {∅} := calc +lemma one_def : (1 : V) = {0} := calc (1 : V) = succ ∅ := rfl _ = {∅} := by simp [succ] +lemma one_def' : (1 : V) = {∅} := one_def + +lemma two_def : (2 : V) = {0, 1} := calc + (2 : V) = succ 1 := rfl + _ = insert 1 1 := by rfl + _ = {1, 0} := by rw [←one_def] + _ = {0, 1} := by ext; simp; tauto + +@[simp] lemma zero_ne_one : (0 : V) ≠ (1 : V) := by + suffices ∅ ≠ {∅} by simpa [zero_def, one_def] + intro e + have := mem_ext_iff.mp e ∅ + simp at this + +@[simp] lemma one_ne_zero : (1 : V) ≠ (0 : V) := Ne.symm zero_ne_one + +@[simp] lemma mem_two_iff (x : V) : x ∈ (2 : V) ↔ x = 0 ∨ x = 1 := by simp [two_def] + @[simp] lemma zero_mem_one : 0 ∈ (1 : V) := by simp [zero_def, one_def] @[simp] lemma ofNat_mem_ω (n : ℕ) : ↑n ∈ (ω : V) := @@ -805,6 +823,4 @@ lemma mem_asymm₃ {x y z : V} : x ∈ y → y ∈ z → z ∉ x := by have : x ∈ succ x := mem_succ_self x simp [←h] at this -@[simp] lemma zero_ne_one : (0 : V) ≠ (1 : V) := ne_succ 0 - end LO.Zermelo diff --git a/Foundation/FirstOrder/Z/Function.lean b/Foundation/FirstOrder/Z/Function.lean index f327de03..5c4add59 100644 --- a/Foundation/FirstOrder/Z/Function.lean +++ b/Foundation/FirstOrder/Z/Function.lean @@ -48,7 +48,7 @@ lemma domain_subset_of_subset_prod {R X Y : V} (h : R ⊆ X ×ˢ Y) : domain R have : x ∈ X ∧ y ∈ Y := by simpa using h _ hy exact this.1 -@[simp, grind =] lemma domain_insert {x y R : V} : domain (Insert.insert (⟨x, y⟩ₖ) R) = Insert.insert x (domain R) := by +@[simp, grind =] lemma domain_insert {x y R : V} : domain (insert (⟨x, y⟩ₖ) R) = insert x (domain R) := by ext z; simp only [mem_domain_iff, mem_insert, kpair_iff]; grind end domain @@ -85,7 +85,7 @@ lemma range_subset_of_subset_prod {R X Y : V} (h : R ⊆ X ×ˢ Y) : range R ⊆ have : x ∈ X ∧ y ∈ Y := by simpa using h _ hx exact this.2 -@[simp, grind =] lemma range_insert {x y R : V} : range (Insert.insert (⟨x, y⟩ₖ) R) = Insert.insert y (range R) := by +@[simp, grind =] lemma range_insert {x y R : V} : range (insert (⟨x, y⟩ₖ) R) = insert y (range R) := by ext z; simp only [mem_range_iff, mem_insert, kpair_iff]; grind end range @@ -112,6 +112,9 @@ lemma mem_function.intro {f X Y : V} (prod : f ⊆ X ×ˢ Y) (total : ∀ x ∈ lemma subset_prod_of_mem_function {f X Y : V} (h : f ∈ Y ^ X) : f ⊆ X ×ˢ Y := mem_function_iff.mp h |>.1 +lemma mem_of_mem_functions {f X Y : V} (h : f ∈ Y ^ X) (hx : ⟨x, y⟩ₖ ∈ f) : x ∈ X ∧ y ∈ Y := by + simpa using subset_prod_of_mem_function h _ hx + lemma function_subset_power_prod (X Y : V) : Y ^ X ⊆ ℘ (X ×ˢ Y) := fun f hf ↦ by simpa using subset_prod_of_mem_function hf lemma exists_unique_of_mem_function {f X Y : V} (h : f ∈ Y ^ X) : ∀ x ∈ X, ∃! y, ⟨x, y⟩ₖ ∈ f := mem_function_iff.mp h |>.2 @@ -119,7 +122,7 @@ lemma exists_unique_of_mem_function {f X Y : V} (h : f ∈ Y ^ X) : ∀ x ∈ X, lemma exists_of_mem_function {f X Y : V} (h : f ∈ Y ^ X) : ∀ x ∈ X, ∃ y ∈ Y, ⟨x, y⟩ₖ ∈ f := by intro x hx rcases (exists_unique_of_mem_function h x hx).exists with ⟨y, hy⟩ - have : x ∈ X ∧ y ∈ Y := by simpa using subset_prod_of_mem_function h _ hy + have : x ∈ X ∧ y ∈ Y := mem_of_mem_functions h hy exact ⟨y, this.2, hy⟩ lemma domain_eq_of_mem_function {f X Y : V} (h : f ∈ Y ^ X) : domain f = X := by @@ -127,7 +130,7 @@ lemma domain_eq_of_mem_function {f X Y : V} (h : f ∈ Y ^ X) : domain f = X := suffices (∃ y, ⟨x, y⟩ₖ ∈ f) ↔ x ∈ X by simpa [mem_domain_iff] constructor · rintro ⟨y, hxy⟩ - have : x ∈ X ∧ y ∈ Y := by simpa using subset_prod_of_mem_function h _ hxy + have : x ∈ X ∧ y ∈ Y := mem_of_mem_functions h hxy exact this.1 · intro hx rcases exists_of_mem_function h x hx with ⟨y, hy⟩ @@ -137,7 +140,7 @@ lemma range_subset_of_mem_function {f X Y : V} (h : f ∈ Y ^ X) : range f ⊆ Y intro y hy have : ∃ x, ⟨x, y⟩ₖ ∈ f := by simpa [mem_range_iff] using hy rcases this with ⟨x, hxy⟩ - have : x ∈ X ∧ y ∈ Y := by simpa using subset_prod_of_mem_function h _ hxy + have : x ∈ X ∧ y ∈ Y := mem_of_mem_functions h hxy exact this.2 lemma mem_function_range_of_mem_function {f X Y : V} (h : f ∈ Y ^ X) : f ∈ range f ^ X := by @@ -203,8 +206,8 @@ lemma unique {f : V} [hf : IsFunction f] {x y₁ y₂} (h₁ : ⟨x, y₁⟩ₖ @[simp] instance empty : IsFunction (∅ : V) := ⟨∅, ∅, by simp⟩ -def insert (f x y : V) (hx : x ∉ domain f) [hf : IsFunction f] : IsFunction (Insert.insert (⟨x, y⟩ₖ) f) := by - refine ⟨Insert.insert x (domain f), Insert.insert y (range f), ?_⟩ +protected def insert (f x y : V) (hx : x ∉ domain f) [hf : IsFunction f] : IsFunction (insert ⟨x, y⟩ₖ f) := by + refine ⟨insert x (domain f), insert y (range f), ?_⟩ apply mem_function.intro · have : f ⊆ domain f ×ˢ range f := subset_prod_of_mem_function hf.mem_function exact insert_kpair_subset_insert_prod_insert_of_subset_prod this x y @@ -225,10 +228,42 @@ def insert (f x y : V) (hx : x ∉ domain f) [hf : IsFunction f] : IsFunction (I contradiction exact hf.unique Hw hzv -@[simp] instance (x y : V) : IsFunction ({⟨x, y⟩ₖ} : V) := by simpa using insert ∅ x y (by simp) +@[simp] instance (x y : V) : IsFunction ({⟨x, y⟩ₖ} : V) := by simpa using IsFunction.insert ∅ x y (by simp) end IsFunction +lemma function_eq_of_subset {X Y f g : V} (hf : f ∈ Y ^ X) (hg : g ∈ Y ^ X) (h : f ⊆ g) : f = g := by + have : IsFunction f := IsFunction.of_mem hf + have : IsFunction g := IsFunction.of_mem hg + apply subset_antisymm h + intro p hp + rcases show ∃ x ∈ X, ∃ y ∈ Y, p = ⟨x, y⟩ₖ from by + simpa [mem_prod_iff] using subset_prod_of_mem_function hg _ hp with ⟨x, hx, y, hy, rfl⟩ + rcases show ∃ y' ∈ Y, ⟨x, y'⟩ₖ ∈ f from exists_of_mem_function hf x hx with ⟨y', hy', Hf⟩ + have : ⟨x, y'⟩ₖ ∈ g := h _ Hf + rcases show y = y' from IsFunction.unique hp (h _ Hf) + assumption + +lemma function_ext {X Y f g : V} (hf : f ∈ Y ^ X) (hg : g ∈ Y ^ X) + (h : ∀ x ∈ X, ∀ y ∈ Y, ⟨x, y⟩ₖ ∈ f → ⟨x, y⟩ₖ ∈ g) : f = g := by + apply function_eq_of_subset hf hg + intro p hp + rcases show ∃ x ∈ X, ∃ y ∈ Y, p = ⟨x, y⟩ₖ from by + simpa [mem_prod_iff] using subset_prod_of_mem_function hf _ hp with ⟨x, hx, y, hy, rfl⟩ + exact h x hx y hy hp + +@[grind] lemma two_val_function_mem_iff_not {X f x : V} (hf : f ∈ (2 ^ X : V)) (hx : x ∈ X) : ⟨x, 0⟩ₖ ∈ f ↔ ⟨x, 1⟩ₖ ∉ f := by + have : IsFunction f := IsFunction.of_mem hf + constructor + · intro h0 h1 + have : (0 : V) = 1 := IsFunction.unique h0 h1 + simp_all + · intro h1 + rcases exists_of_mem_function hf x hx with ⟨i, hi, hf⟩ + rcases show i = 0 ∨ i = 1 by simpa using hi with (rfl | rfl) + · assumption + · contradiction + def Injective (R : V) : Prop := ∀ x₁ x₂ y, ⟨x₁, y⟩ₖ ∈ R → ⟨x₂, y⟩ₖ ∈ R → x₁ = x₂ def Injective.dfn : Semisentence ℒₛₑₜ 1 := f“f. ∀ x₁ x₂ y, !kpair.dfn x₁ y ∈ f → !kpair.dfn x₂ y ∈ f → x₁ = x₂” @@ -374,6 +409,81 @@ instance CardEQ.definable : ℒₛₑₜ-relation[V] (· ≋ ·) := defined.to_d @[simp, refl] lemma CardEQ.refl (X : V) : X ≋ X := ⟨by rfl, by rfl⟩ -@[simp, symm] lemma CardEQ.symm {X Y : V} : X ≋ Y → Y ≋ X := fun e ↦ ⟨e.2, e.1⟩ +@[symm] lemma CardEQ.symm {X Y : V} : X ≋ Y → Y ≋ X := fun e ↦ ⟨e.2, e.1⟩ + +lemma two_pow_cardEQ_power (X : V) : 2 ^ X ≋ ℘ X := by + constructor + · let F : V := {p ∈ (2 ^ X) ×ˢ ℘ X ; ∃ f s, p = ⟨f, s⟩ₖ ∧ ∀ x, x ∈ s ↔ ⟨x, 1⟩ₖ ∈ f} + refine ⟨F, ?_, ?_⟩ + · apply mem_function.intro + · simp [F] + · intro f hf + let s : V := {x ∈ X ; ⟨x, 1⟩ₖ ∈ f} + have ss_s : s ⊆ X := by simp [s] + have mem_s : ∀ x, x ∈ s ↔ ⟨x, 1⟩ₖ ∈ f := by + simp only [mem_sep_iff, and_iff_right_iff_imp, s] + intro x hx + exact mem_of_mem_functions hf hx |>.1 + apply ExistsUnique.intro s ?_ ?_ + · simp [F, hf, ss_s, mem_s] + · intro t ht + ext x + have ht : (f ∈ ((2 : V) ^ X) ∧ t ⊆ X) ∧ ∀ x, x ∈ t ↔ ⟨x, 1⟩ₖ ∈ f := by simpa [F] using ht + simp [ht, mem_s] + · intro f₁ f₂ s h₁ h₂ + have : (f₁ ∈ (2 ^ X : V) ∧ s ⊆ X) ∧ ∀ x, x ∈ s ↔ ⟨x, 1⟩ₖ ∈ f₁ := by simpa [F] using h₁ + rcases this with ⟨⟨f₁func, hs⟩, H₁⟩ + have : (f₂ ∈ (2 ^ X : V) ∧ s ⊆ X) ∧ ∀ x, x ∈ s ↔ ⟨x, 1⟩ₖ ∈ f₂ := by simpa [F] using h₂ + rcases this with ⟨⟨f₂func, _⟩, H₂⟩ + apply function_ext f₁func f₂func + intro x hx i hi + rcases show i = 0 ∨ i = 1 by simpa using hi with (rfl | rfl) + · contrapose + suffices ⟨x, 1⟩ₖ ∈ f₂ → ⟨x, 1⟩ₖ ∈ f₁ by grind + grind + · grind + · let F : V := {p ∈ ℘ X ×ˢ (2 ^ X) ; ∃ f s, p = ⟨s, f⟩ₖ ∧ ∀ x, ⟨x, 1⟩ₖ ∈ f ↔ x ∈ s} + refine ⟨F, ?_, ?_⟩ + · apply mem_function.intro + · simp [F] + · intro s hs + have hs : s ⊆ X := by simpa using hs + let f : V := {p ∈ X ×ˢ 2 ; ∃ x, (x ∈ s → p = ⟨x, 1⟩ₖ) ∧ (x ∉ s → p = ⟨x, 0⟩ₖ)} + have kp1_mem_f : ∀ x, ⟨x, 1⟩ₖ ∈ f ↔ x ∈ s := by + intro x + have : x ∈ s → x ∈ X := fun hx ↦ hs _ hx + simp only [mem_sep_iff, kpair_mem_iff, mem_two_iff, one_ne_zero, or_true, and_true, + kpair_iff, and_false, imp_false, not_not, f]; grind + have f_func : f ∈ (2 ^ X : V) := by + apply mem_function.intro (by simp [f]) + intro x hx + by_cases hxS : x ∈ s + · apply ExistsUnique.intro 1 + · simp only [mem_sep_iff, kpair_mem_iff, hx, mem_two_iff, one_ne_zero, or_true, and_self, + kpair_iff, and_true, and_false, imp_false, not_not, true_and, f]; grind + · intro i hi + simp [f, hx] at hi + grind only + · apply ExistsUnique.intro 0 + · simp only [mem_sep_iff, kpair_mem_iff, hx, mem_two_iff, zero_ne_one, or_false, + and_self, kpair_iff, and_false, imp_false, and_true, true_and, f]; grind + · intro i hi + simp [f, hx] at hi + grind + apply ExistsUnique.intro f ?_ ?_ + · simp [F, hs, kp1_mem_f, f_func] + · intro g hg + have : (s ⊆ X ∧ g ∈ (2 ^ X : V)) ∧ ∀ (x : V), ⟨x, 1⟩ₖ ∈ g ↔ x ∈ s := by simpa [F] using hg + rcases this with ⟨⟨_, g_func⟩, Hg⟩ + apply function_ext g_func f_func + intro x hx i hi + rcases show i = 0 ∨ i = 1 by simpa using hi with (rfl | rfl) + · suffices ⟨x, 1⟩ₖ ∈ f → ⟨x, 1⟩ₖ ∈ g by grind + grind + · grind + · intro s₁ s₂ f h₁ h₂ + have : (s₁ ⊆ X ∧ f ∈ (2 ^ X : V)) ∧ ∀ (x : V), ⟨x, 1⟩ₖ ∈ f ↔ x ∈ s₁ := by simpa [F] using h₁ + have : (s₂ ⊆ X ∧ f ∈ (2 ^ X : V)) ∧ ∀ (x : V), ⟨x, 1⟩ₖ ∈ f ↔ x ∈ s₂ := by simpa [F] using h₂ + ext z; grind end LO.Zermelo From 1f05cafbaf8dd366c01d4c71379dc4eac016e04a Mon Sep 17 00:00:00 2001 From: palalansouki Date: Sun, 5 Oct 2025 16:29:55 +0900 Subject: [PATCH 2/3] fix --- Foundation/FirstOrder/Z/Function.lean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/Foundation/FirstOrder/Z/Function.lean b/Foundation/FirstOrder/Z/Function.lean index 5c4add59..bdb4a38a 100644 --- a/Foundation/FirstOrder/Z/Function.lean +++ b/Foundation/FirstOrder/Z/Function.lean @@ -407,10 +407,17 @@ instance CardEQ.defined : ℒₛₑₜ-relation[V] (· ≋ ·) via dfn := ⟨fun instance CardEQ.definable : ℒₛₑₜ-relation[V] (· ≋ ·) := defined.to_definable +lemma CardEQ.le {X Y : V} (h : X ≋ Y) : X ≤ Y := h.1 + +lemma CardEQ.ge {X Y : V} (h : X ≋ Y) : X ≥ Y := h.2 + @[simp, refl] lemma CardEQ.refl (X : V) : X ≋ X := ⟨by rfl, by rfl⟩ @[symm] lemma CardEQ.symm {X Y : V} : X ≋ Y → Y ≋ X := fun e ↦ ⟨e.2, e.1⟩ +@[trans] lemma CardEQ.trans {X Y Z : V} : X ≋ Y → Y ≋ Z → X ≋ Z := fun eXY eYZ ↦ + ⟨eXY.le.trans eYZ.le, eYZ.ge.trans eXY.ge⟩ + lemma two_pow_cardEQ_power (X : V) : 2 ^ X ≋ ℘ X := by constructor · let F : V := {p ∈ (2 ^ X) ×ˢ ℘ X ; ∃ f s, p = ⟨f, s⟩ₖ ∧ ∀ x, x ∈ s ↔ ⟨x, 1⟩ₖ ∈ f} From 2ee4e96fd4ecb88961883e691f62fecbc38db0c6 Mon Sep 17 00:00:00 2001 From: palalansouki Date: Mon, 6 Oct 2025 06:03:55 +0900 Subject: [PATCH 3/3] cardLT_power --- Foundation/FirstOrder/Z/Basic.lean | 5 ++ Foundation/FirstOrder/Z/Function.lean | 77 +++++++++++++++++++-------- 2 files changed, 59 insertions(+), 23 deletions(-) diff --git a/Foundation/FirstOrder/Z/Basic.lean b/Foundation/FirstOrder/Z/Basic.lean index 5ed62e1f..026b53f7 100644 --- a/Foundation/FirstOrder/Z/Basic.lean +++ b/Foundation/FirstOrder/Z/Basic.lean @@ -199,6 +199,11 @@ instance singleton.definable : ℒₛₑₜ-function₁[V] Singleton.singleton : @[simp] instance singleton_isNonempty (x : V) : IsNonempty ({x} : V) := ⟨x, by simp⟩ +@[simp] lemma singleton_subset_iff_mem {x y : V} : {x} ⊆ y ↔ x ∈ y := by simp [subset_def] + +@[simp] lemma singleton_ext_iff {x y : V} : ({x} : V) = {y} ↔ x = y := by + simp [mem_ext_iff (x := {x})] + /-! ## Axiom of union -/ lemma union_exists : ∀ x : V, ∃ y : V, ∀ z, z ∈ y ↔ ∃ w ∈ x, z ∈ w := by diff --git a/Foundation/FirstOrder/Z/Function.lean b/Foundation/FirstOrder/Z/Function.lean index bdb4a38a..5b1c09dc 100644 --- a/Foundation/FirstOrder/Z/Function.lean +++ b/Foundation/FirstOrder/Z/Function.lean @@ -363,53 +363,49 @@ lemma compose_injective {R S : V} (hR : Injective R) (hS : Injective S) : Inject def CardLE (X Y : V) : Prop := ∃ f ∈ Y ^ X, Injective f -scoped instance : LE V := ⟨CardLE⟩ +infix:50 " ≤# " => CardLE -lemma cardLE_of_subset {X Y : V} (h : X ⊆ Y) : X ≤ Y := +lemma cardLE_of_subset {X Y : V} (h : X ⊆ Y) : X ≤# Y := ⟨identity X, mem_function_of_mem_function_of_subset (identity_mem_function X) h, by simp⟩ -@[simp] lemma cardLE_empty (X : V) : ∅ ≤ X := cardLE_of_subset (by simp) +@[simp] lemma cardLE_empty (X : V) : ∅ ≤# X := cardLE_of_subset (by simp) -@[simp, refl] lemma CardLE.refl (X : V) : X ≤ X := cardLE_of_subset (by simp) +@[simp, refl] lemma CardLE.refl (X : V) : X ≤# X := cardLE_of_subset (by simp) -@[trans] lemma CardLE.trans {X Y Z : V} : X ≤ Y → Y ≤ Z → X ≤ Z := by +@[trans] lemma CardLE.trans {X Y Z : V} : X ≤# Y → Y ≤# Z → X ≤# Z := by rintro ⟨f, hf, f_inj⟩ rintro ⟨g, hg, g_inj⟩ refine ⟨compose f g, compose_function hf hg, compose_injective f_inj g_inj⟩ -instance : Preorder V where - le_refl := CardLE.refl - le_trans _ _ _ := CardLE.trans +def CardLT (X Y : V) : Prop := X ≤# Y ∧ ¬Y ≤# X -lemma cardLE_def {X Y : V} : X ≤ Y ↔ ∃ f ∈ Y ^ X, Injective f := by rfl - -lemma cardLT_def {X Y : V} : X < Y ↔ X ≤ Y ∧ ¬Y ≤ X := by rfl +infix:50 " <# " => CardLT def CardLE.dfn : Semisentence ℒₛₑₜ 2 := f“X Y. ∃ f ∈ !function.dfn Y X, !Injective.dfn f” -instance CardLE.defined : ℒₛₑₜ-relation[V] (· ≤ ·) via dfn := ⟨fun v ↦ by simp [cardLE_def, dfn]⟩ +instance CardLE.defined : ℒₛₑₜ-relation[V] CardLE via dfn := ⟨fun v ↦ by simp [CardLE, dfn]⟩ -instance CardLE.definable : ℒₛₑₜ-relation[V] (· ≤ ·) := defined.to_definable +instance CardLE.definable : ℒₛₑₜ-relation[V] CardLE := defined.to_definable def CardLT.dfn : Semisentence ℒₛₑₜ 2 := “X Y. !CardLE.dfn X Y ∧ ¬!CardLE.dfn Y X” -instance CardLT.defined : ℒₛₑₜ-relation[V] (· < ·) via dfn := ⟨fun v ↦ by simp [cardLT_def, dfn]⟩ +instance CardLT.defined : ℒₛₑₜ-relation[V] CardLT via dfn := ⟨fun v ↦ by simp [CardLT, dfn]⟩ -instance CardLT.definable : ℒₛₑₜ-relation[V] (· < ·) := defined.to_definable +instance CardLT.definable : ℒₛₑₜ-relation[V] CardLT := defined.to_definable -def CardEQ (X Y : V) : Prop := X ≤ Y ∧ Y ≤ X +def CardEQ (X Y : V) : Prop := X ≤# Y ∧ Y ≤# X infix:60 " ≋ " => CardEQ def CardEQ.dfn : Semisentence ℒₛₑₜ 2 := “X Y. !CardLE.dfn X Y ∧ !CardLE.dfn Y X” -instance CardEQ.defined : ℒₛₑₜ-relation[V] (· ≋ ·) via dfn := ⟨fun v ↦ by simp [CardEQ, dfn]⟩ +instance CardEQ.defined : ℒₛₑₜ-relation[V] CardEQ via dfn := ⟨fun v ↦ by simp [CardEQ, dfn]⟩ -instance CardEQ.definable : ℒₛₑₜ-relation[V] (· ≋ ·) := defined.to_definable +instance CardEQ.definable : ℒₛₑₜ-relation[V] CardEQ := defined.to_definable -lemma CardEQ.le {X Y : V} (h : X ≋ Y) : X ≤ Y := h.1 +lemma CardEQ.le {X Y : V} (h : X ≋ Y) : X ≤# Y := h.1 -lemma CardEQ.ge {X Y : V} (h : X ≋ Y) : X ≥ Y := h.2 +lemma CardEQ.ge {X Y : V} (h : X ≋ Y) : Y ≤# X := h.2 @[simp, refl] lemma CardEQ.refl (X : V) : X ≋ X := ⟨by rfl, by rfl⟩ @@ -418,6 +414,41 @@ lemma CardEQ.ge {X Y : V} (h : X ≋ Y) : X ≥ Y := h.2 @[trans] lemma CardEQ.trans {X Y Z : V} : X ≋ Y → Y ≋ Z → X ≋ Z := fun eXY eYZ ↦ ⟨eXY.le.trans eYZ.le, eYZ.ge.trans eXY.ge⟩ +lemma cardLT_power (X : V) : X <# ℘ X := by + have : X ≤# ℘ X := by + let F : V := {p ∈ X ×ˢ ℘ X ; ∃ x ∈ X, p = ⟨x, {x}⟩ₖ} + have : F ∈ ℘ X ^ X := by + apply mem_function.intro + · simp [F] + · intro x hx + apply ExistsUnique.intro {x} (by simp [F, hx]) + intro y hy + have : y ⊆ X ∧ y = {x} := by simpa [hx, F] using hy + simp [this] + have : Injective F := by + intro x₁ x₂ s h₁ h₂ + rcases show (x₁ ∈ X ∧ s ⊆ X) ∧ x₁ ∈ X ∧ s = {x₁} by simpa [F] using h₁ with ⟨_, _, rfl⟩ + have : (x₂ ∈ X ∧ x₁ ∈ X) ∧ x₁ ∈ X ∧ x₂ = x₁ := by simpa [F] using h₂ + simp [this.2.2] + refine ⟨F, by assumption, by assumption⟩ + have : ¬℘ X ≤# X := by + rintro ⟨F, hF, injF⟩ + have : IsFunction F := IsFunction.of_mem hF + let D : V := {x ∈ X ; ∃ s ∈ ℘ X, ⟨s, x⟩ₖ ∈ F ∧ x ∉ s} + have : ∃ d ∈ X, ⟨D, d⟩ₖ ∈ F := exists_of_mem_function hF D (by simp [D]) + rcases this with ⟨d, hd, Hd⟩ + have : d ∈ D ↔ d ∉ D := calc + d ∈ D ↔ ∃ s ⊆ X, ⟨s, d⟩ₖ ∈ F ∧ d ∉ s := by simp [hd, D] + _ ↔ d ∉ D := ?_ + · grind + constructor + · rintro ⟨S, hS, hSF, hdS⟩ + rcases show D = S from injF _ _ _ Hd hSF + assumption + · intro h + refine ⟨D, by simpa [hd] using mem_of_mem_functions hF Hd, Hd, h⟩ + refine ⟨by assumption, by assumption⟩ + lemma two_pow_cardEQ_power (X : V) : 2 ^ X ≋ ℘ X := by constructor · let F : V := {p ∈ (2 ^ X) ×ˢ ℘ X ; ∃ f s, p = ⟨f, s⟩ₖ ∧ ∀ x, x ∈ s ↔ ⟨x, 1⟩ₖ ∈ f} @@ -480,7 +511,7 @@ lemma two_pow_cardEQ_power (X : V) : 2 ^ X ≋ ℘ X := by apply ExistsUnique.intro f ?_ ?_ · simp [F, hs, kp1_mem_f, f_func] · intro g hg - have : (s ⊆ X ∧ g ∈ (2 ^ X : V)) ∧ ∀ (x : V), ⟨x, 1⟩ₖ ∈ g ↔ x ∈ s := by simpa [F] using hg + have : (s ⊆ X ∧ g ∈ (2 ^ X : V)) ∧ ∀ x, ⟨x, 1⟩ₖ ∈ g ↔ x ∈ s := by simpa [F] using hg rcases this with ⟨⟨_, g_func⟩, Hg⟩ apply function_ext g_func f_func intro x hx i hi @@ -489,8 +520,8 @@ lemma two_pow_cardEQ_power (X : V) : 2 ^ X ≋ ℘ X := by grind · grind · intro s₁ s₂ f h₁ h₂ - have : (s₁ ⊆ X ∧ f ∈ (2 ^ X : V)) ∧ ∀ (x : V), ⟨x, 1⟩ₖ ∈ f ↔ x ∈ s₁ := by simpa [F] using h₁ - have : (s₂ ⊆ X ∧ f ∈ (2 ^ X : V)) ∧ ∀ (x : V), ⟨x, 1⟩ₖ ∈ f ↔ x ∈ s₂ := by simpa [F] using h₂ + have : (s₁ ⊆ X ∧ f ∈ (2 ^ X : V)) ∧ ∀ x, ⟨x, 1⟩ₖ ∈ f ↔ x ∈ s₁ := by simpa [F] using h₁ + have : (s₂ ⊆ X ∧ f ∈ (2 ^ X : V)) ∧ ∀ x, ⟨x, 1⟩ₖ ∈ f ↔ x ∈ s₂ := by simpa [F] using h₂ ext z; grind end LO.Zermelo