Imports
import Mathlib.Tactic
import Analysis.Section_8_1
import Analysis.Section_8_2Analysis I, Section 8.3: Uncountable sets
I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.
Main constructions and results of this section:
-
Uncountable sets.
Some non-trivial API is provided beyond what is given in the textbook in order connect these notions with existing summation notions.
namespace Chapter8Theorem 8.3.1
theorem EqualCard.power_set_false (X:Type) : ¬ EqualCard X (Set X) := X:Type⊢ ¬EqualCard X (Set X)
-- This proof is written to follow the structure of the original text.
X:Typethis:EqualCard X (Set X)⊢ False; X:Typef:X → Set Xhf:Function.Bijective f⊢ False
X:Typef:X → Set Xhf:Function.Bijective fA:Set X := {x | x ∉ f x}⊢ False; X:Typef:X → Set Xhf:Function.Bijective fA:Set X := {x | x ∉ f x}x:Xhx:f x = A⊢ False
X:Typef:X → Set Xhf:Function.Bijective fA:Set X := {x | x ∉ f x}x:Xhx:f x = Ah:x ∈ A⊢ FalseX:Typef:X → Set Xhf:Function.Bijective fA:Set X := {x | x ∉ f x}x:Xhx:f x = Ah:x ∉ A⊢ False X:Typef:X → Set Xhf:Function.Bijective fA:Set X := {x | x ∉ f x}x:Xhx:f x = Ah:x ∈ A⊢ FalseX:Typef:X → Set Xhf:Function.Bijective fA:Set X := {x | x ∉ f x}x:Xhx:f x = Ah:x ∉ A⊢ False X:Typef:X → Set Xhf:Function.Bijective fA:Set X := {x | x ∉ f x}x:Xhx:f x = Ah:x ∉ Ah':x ∉ A⊢ False
X:Typef:X → Set Xhf:Function.Bijective fA:Set X := {x | x ∉ f x}x:Xhx:f x = Ah:x ∈ Ah':x ∈ A⊢ False X:Typef:X → Set Xhf:Function.Bijective fA:Set X := {x | x ∉ f x}x:Xhx:f x = Ah:x ∈ Ah':x ∉ f x⊢ False; All goals completed! 🐙
X:Typef:X → Set Xhf:Function.Bijective fA:Set X := {x | x ∉ f x}x:Xhx:f x = Ah:x ∉ Ah':x ∉ f x⊢ False
have : x ∈ A := X:Type⊢ ¬EqualCard X (Set X) All goals completed! 🐙
All goals completed! 🐙theorem Uncountable.iff (X:Type) : Uncountable X ↔ ¬ AtMostCountable X := X:Type⊢ Uncountable X ↔ ¬AtMostCountable X
All goals completed! 🐙theorem Uncountable.equiv {X Y: Type} (hXY : EqualCard X Y) :
Uncountable X ↔ Uncountable Y := X:TypeY:TypehXY:EqualCard X Y⊢ Uncountable X ↔ Uncountable Y
All goals completed! 🐙Corollary 8.3.3
theorem Uncountable.power_set_nat : Uncountable (Set ℕ) := ⊢ Uncountable (Set ℕ)
-- This proof is written to follow the structure of the original text.
⊢ ¬AtMostCountable (Set ℕ)
⊢ ¬(CountablyInfinite (Set ℕ) ∨ Finite (Set ℕ))
have : ¬ CountablyInfinite (Set ℕ) := ⊢ Uncountable (Set ℕ)
this:¬EqualCard ℕ (Set ℕ)⊢ ¬CountablyInfinite (Set ℕ)
this:CountablyInfinite (Set ℕ)⊢ EqualCard ℕ (Set ℕ); All goals completed! 🐙
have : ¬ Finite (Set ℕ) := ⊢ Uncountable (Set ℕ)
this✝:¬CountablyInfinite (Set ℕ)this:Finite (Set ℕ)⊢ False
have : Finite ((fun x:ℕ ↦ ({x}:Set ℕ)) '' .univ) := Finite.Set.subset (s := .univ) (this✝:¬CountablyInfinite (Set ℕ)this:Finite (Set ℕ)⊢ (fun x ↦ {x}) '' Set.univ ⊆ Set.univ All goals completed! 🐙)
replace : Finite ℕ := ⊢ Uncountable (Set ℕ)
this✝¹:¬CountablyInfinite (Set ℕ)this✝:Finite (Set ℕ)this:Finite ↑((fun x ↦ {x}) '' Set.univ)⊢ Set.univ.Finite
this✝¹:¬CountablyInfinite (Set ℕ)this✝:Finite (Set ℕ)this:Finite ↑((fun x ↦ {x}) '' Set.univ)⊢ Finite ↑Set.univ
this✝¹:¬CountablyInfinite (Set ℕ)this✝:Finite (Set ℕ)this:Finite ↑((fun x ↦ {x}) '' Set.univ)⊢ Set.InjOn (fun x ↦ {x}) Set.univ
intro _ this✝¹:¬CountablyInfinite (Set ℕ)this✝:Finite (Set ℕ)this:Finite ↑((fun x ↦ {x}) '' Set.univ)x₁✝:ℕa✝:x₁✝ ∈ Set.univ⊢ ∀ ⦃x₂ : ℕ⦄, x₂ ∈ Set.univ → (fun x ↦ {x}) x₁✝ = (fun x ↦ {x}) x₂ → x₁✝ = x₂ this✝¹:¬CountablyInfinite (Set ℕ)this✝:Finite (Set ℕ)this:Finite ↑((fun x ↦ {x}) '' Set.univ)x₁✝:ℕa✝:x₁✝ ∈ Set.univx₂✝:ℕ⊢ x₂✝ ∈ Set.univ → (fun x ↦ {x}) x₁✝ = (fun x ↦ {x}) x₂✝ → x₁✝ = x₂✝ this✝¹:¬CountablyInfinite (Set ℕ)this✝:Finite (Set ℕ)this:Finite ↑((fun x ↦ {x}) '' Set.univ)x₁✝:ℕa✝¹:x₁✝ ∈ Set.univx₂✝:ℕa✝:x₂✝ ∈ Set.univ⊢ (fun x ↦ {x}) x₁✝ = (fun x ↦ {x}) x₂✝ → x₁✝ = x₂✝ this✝¹:¬CountablyInfinite (Set ℕ)this✝:Finite (Set ℕ)this:Finite ↑((fun x ↦ {x}) '' Set.univ)x₁✝:ℕa✝²:x₁✝ ∈ Set.univx₂✝:ℕa✝¹:x₂✝ ∈ Set.univa✝:(fun x ↦ {x}) x₁✝ = (fun x ↦ {x}) x₂✝⊢ x₁✝ = x₂✝; All goals completed! 🐙
have hinf : ¬ Finite ℕ := ⊢ Uncountable (Set ℕ) this✝¹:¬CountablyInfinite (Set ℕ)this✝:Finite (Set ℕ)this:Finite ℕ⊢ Infinite ℕ; All goals completed! 🐙
All goals completed! 🐙
All goals completed! 🐙Corollary 8.3.4
open Real intheorem Uncountable.real : Uncountable ℝ := ⊢ Uncountable ℝ
-- This proof is written to follow the structure of the original text.
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)⊢ Uncountable ℝ
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑n⊢ Uncountable ℝ
have hsummable (A: Set ℕ) : Summable (fun n:A ↦ a n) := ⊢ Uncountable ℝ
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nA:Set ℕ⊢ Summable a
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nA:Set ℕn:ℕ⊢ a n = (1 / 10) ^ na:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nA:Set ℕ⊢ 0 ≤ 1 / 10a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nA:Set ℕ⊢ 1 / 10 < 1 a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nA:Set ℕn:ℕ⊢ a n = (1 / 10) ^ na:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nA:Set ℕ⊢ 0 ≤ 1 / 10a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nA:Set ℕ⊢ 1 / 10 < 1 try All goals completed! 🐙
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nA:Set ℕn:ℕ⊢ 10 ^ (-↑n) = (1 / 10) ^ n
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nA:Set ℕn:ℕ⊢ (10 ^ ↑n)⁻¹ = (10 ^ n)⁻¹a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nA:Set ℕn:ℕ⊢ 0 ≤ 10; a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nA:Set ℕn:ℕ⊢ 0 ≤ 10; All goals completed! 🐙
have h_decomp {A B C: Set ℕ} (hC : C = A ∪ B) (hAB: ∀ n, n ∉ A ∩ B) : ∑' n:C, a n = ∑' n:A, a n + ∑' n:B, a n := ⊢ Uncountable ℝ
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nA:Set ℕB:Set ℕC:Set ℕhC:C = A ∪ BhAB:∀ (n : ℕ), n ∉ A ∩ B⊢ ∑' (n : ↑C), a ↑n = ∑' (x : ↑(A ∪ B)), a ↑xa:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nA:Set ℕB:Set ℕC:Set ℕhC:C = A ∪ BhAB:∀ (n : ℕ), n ∉ A ∩ B⊢ T2Space ℝa:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nA:Set ℕB:Set ℕC:Set ℕhC:C = A ∪ BhAB:∀ (n : ℕ), n ∉ A ∩ B⊢ ContinuousAdd ℝa:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nA:Set ℕB:Set ℕC:Set ℕhC:C = A ∪ BhAB:∀ (n : ℕ), n ∉ A ∩ B⊢ Disjoint A Ba:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nA:Set ℕB:Set ℕC:Set ℕhC:C = A ∪ BhAB:∀ (n : ℕ), n ∉ A ∩ B⊢ Summable (a ∘ Subtype.val)a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nA:Set ℕB:Set ℕC:Set ℕhC:C = A ∪ BhAB:∀ (n : ℕ), n ∉ A ∩ B⊢ Summable (a ∘ Subtype.val) a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nA:Set ℕB:Set ℕC:Set ℕhC:C = A ∪ BhAB:∀ (n : ℕ), n ∉ A ∩ B⊢ ∑' (n : ↑C), a ↑n = ∑' (x : ↑(A ∪ B)), a ↑xa:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nA:Set ℕB:Set ℕC:Set ℕhC:C = A ∪ BhAB:∀ (n : ℕ), n ∉ A ∩ B⊢ T2Space ℝa:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nA:Set ℕB:Set ℕC:Set ℕhC:C = A ∪ BhAB:∀ (n : ℕ), n ∉ A ∩ B⊢ ContinuousAdd ℝa:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nA:Set ℕB:Set ℕC:Set ℕhC:C = A ∪ BhAB:∀ (n : ℕ), n ∉ A ∩ B⊢ Disjoint A Ba:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nA:Set ℕB:Set ℕC:Set ℕhC:C = A ∪ BhAB:∀ (n : ℕ), n ∉ A ∩ B⊢ Summable (a ∘ Subtype.val)a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nA:Set ℕB:Set ℕC:Set ℕhC:C = A ∪ BhAB:∀ (n : ℕ), n ∉ A ∩ B⊢ Summable (a ∘ Subtype.val) first | a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nA:Set ℕB:Set ℕC:Set ℕhC:C = A ∪ BhAB:∀ (n : ℕ), n ∉ A ∩ B⊢ Summable (a ∘ Subtype.val) | try All goals completed! 🐙
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nA:Set ℕB:Set ℕC:Set ℕhC:C = A ∪ BhAB:∀ (n : ℕ), n ∉ A ∩ B⊢ ∑' (n : ↑C), a ↑n = ∑' (x : ↑(A ∪ B)), a ↑x All goals completed! 🐙
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nA:Set ℕB:Set ℕC:Set ℕhC:C = A ∪ BhAB:∀ (n : ℕ), n ∉ A ∩ B⊢ A ∩ B = ∅; All goals completed! 🐙
have h_nonneg (A:Set ℕ) : ∑' n:A, a n ≥ 0 := ⊢ Uncountable ℝ a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nA:Set ℕ⊢ 0 ≤ ∑' (n : ↑A), (10 ^ ↑n)⁻¹; All goals completed! 🐙
have h_congr {A B: Set ℕ} (hAB: A = B) : ∑' n:A, a n = ∑' n:B, a n := ⊢ Uncountable ℝ All goals completed! 🐙
have : Function.Injective f := ⊢ Uncountable ℝ
intro A a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕ⊢ f A = f B → A = B a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f B⊢ A = B; a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bthis:A ≠ B⊢ False
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bthis:(symmDiff A B).Nonempty⊢ False
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bthis:Nat.min (symmDiff A B) ∈ symmDiff A B ∧ ∀ n ∈ symmDiff A B, Nat.min (symmDiff A B) ≤ n⊢ False
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)this:n₀ ∈ symmDiff A B ∧ ∀ n ∈ symmDiff A B, n₀ ≤ n⊢ False
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)this:(n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ A) ∧ ∀ (n : ℕ), n ∈ A ∧ n ∉ B ∨ n ∈ B ∧ n ∉ A → n₀ ≤ n⊢ False; a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah2:∀ (n : ℕ), n ∈ A ∧ n ∉ B ∨ n ∈ B ∧ n ∉ A → n₀ ≤ n⊢ False
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah2:∀ (n : ℕ), n ∈ A ∧ n ∉ B ∨ n ∈ B ∧ n ∉ A → n₀ ≤ nthis:∀ ⦃A B : Set ℕ⦄,
f A = f B →
let n₀ := Nat.min (symmDiff A B);
n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ A → (∀ (n : ℕ), n ∈ A ∧ n ∉ B ∨ n ∈ B ∧ n ∉ A → n₀ ≤ n) → n₀ ∈ A ∧ n₀ ∉ B → Falseh:¬(n₀ ∈ A ∧ n₀ ∉ B)⊢ Falsea:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah2:∀ (n : ℕ), n ∈ A ∧ n ∉ B ∨ n ∈ B ∧ n ∉ A → n₀ ≤ nh:n₀ ∈ A ∧ n₀ ∉ B⊢ False
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah2:∀ (n : ℕ), n ∈ A ∧ n ∉ B ∨ n ∈ B ∧ n ∉ A → n₀ ≤ nthis:∀ ⦃A B : Set ℕ⦄,
f A = f B →
let n₀ := Nat.min (symmDiff A B);
n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ A → (∀ (n : ℕ), n ∈ A ∧ n ∉ B ∨ n ∈ B ∧ n ∉ A → n₀ ≤ n) → n₀ ∈ A ∧ n₀ ∉ B → Falseh:¬(n₀ ∈ A ∧ n₀ ∉ B)⊢ False a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h2:∀ (n : ℕ), n ∈ A ∧ n ∉ B ∨ n ∈ B ∧ n ∉ A → n₀ ≤ nthis:∀ ⦃A B : Set ℕ⦄,
f A = f B →
let n₀ := Nat.min (symmDiff A B);
n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ A → (∀ (n : ℕ), n ∈ A ∧ n ∉ B ∨ n ∈ B ∧ n ∉ A → n₀ ≤ n) → n₀ ∈ A ∧ n₀ ∉ B → Falseh:¬(n₀ ∈ A ∧ n₀ ∉ B)h1:n₀ ∈ B ∧ n₀ ∉ A⊢ False
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h2:∀ (n : ℕ), n ∈ A ∧ n ∉ B ∨ n ∈ B ∧ n ∉ A → n₀ ≤ nthis:∀ ⦃A B : Set ℕ⦄,
f A = f B →
let n₀ := Nat.min (symmDiff A B);
n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ A → (∀ (n : ℕ), n ∈ A ∧ n ∉ B ∨ n ∈ B ∧ n ∉ A → n₀ ≤ n) → n₀ ∈ A ∧ n₀ ∉ B → Falseh:¬(n₀ ∈ A ∧ n₀ ∉ B)h1:n₀ ∈ B ∧ n₀ ∉ A⊢ Nat.min (symmDiff B A) ∈ B ∧ Nat.min (symmDiff B A) ∉ A ∨ Nat.min (symmDiff B A) ∈ A ∧ Nat.min (symmDiff B A) ∉ Ba:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h2:∀ (n : ℕ), n ∈ A ∧ n ∉ B ∨ n ∈ B ∧ n ∉ A → n₀ ≤ nthis:∀ ⦃A B : Set ℕ⦄,
f A = f B →
let n₀ := Nat.min (symmDiff A B);
n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ A → (∀ (n : ℕ), n ∈ A ∧ n ∉ B ∨ n ∈ B ∧ n ∉ A → n₀ ≤ n) → n₀ ∈ A ∧ n₀ ∉ B → Falseh:¬(n₀ ∈ A ∧ n₀ ∉ B)h1:n₀ ∈ B ∧ n₀ ∉ A⊢ ∀ (n : ℕ), n ∈ B ∧ n ∉ A ∨ n ∈ A ∧ n ∉ B → Nat.min (symmDiff B A) ≤ na:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h2:∀ (n : ℕ), n ∈ A ∧ n ∉ B ∨ n ∈ B ∧ n ∉ A → n₀ ≤ nthis:∀ ⦃A B : Set ℕ⦄,
f A = f B →
let n₀ := Nat.min (symmDiff A B);
n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ A → (∀ (n : ℕ), n ∈ A ∧ n ∉ B ∨ n ∈ B ∧ n ∉ A → n₀ ≤ n) → n₀ ∈ A ∧ n₀ ∉ B → Falseh:¬(n₀ ∈ A ∧ n₀ ∉ B)h1:n₀ ∈ B ∧ n₀ ∉ A⊢ Nat.min (symmDiff B A) ∈ B ∧ Nat.min (symmDiff B A) ∉ A a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h2:∀ (n : ℕ), n ∈ A ∧ n ∉ B ∨ n ∈ B ∧ n ∉ A → n₀ ≤ nthis:∀ ⦃A B : Set ℕ⦄,
f A = f B →
let n₀ := Nat.min (symmDiff A B);
n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ A → (∀ (n : ℕ), n ∈ A ∧ n ∉ B ∨ n ∈ B ∧ n ∉ A → n₀ ≤ n) → n₀ ∈ A ∧ n₀ ∉ B → Falseh:¬(n₀ ∈ A ∧ n₀ ∉ B)h1:n₀ ∈ B ∧ n₀ ∉ A⊢ Nat.min (symmDiff B A) ∈ B ∧ Nat.min (symmDiff B A) ∉ A ∨ Nat.min (symmDiff B A) ∈ A ∧ Nat.min (symmDiff B A) ∉ Ba:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h2:∀ (n : ℕ), n ∈ A ∧ n ∉ B ∨ n ∈ B ∧ n ∉ A → n₀ ≤ nthis:∀ ⦃A B : Set ℕ⦄,
f A = f B →
let n₀ := Nat.min (symmDiff A B);
n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ A → (∀ (n : ℕ), n ∈ A ∧ n ∉ B ∨ n ∈ B ∧ n ∉ A → n₀ ≤ n) → n₀ ∈ A ∧ n₀ ∉ B → Falseh:¬(n₀ ∈ A ∧ n₀ ∉ B)h1:n₀ ∈ B ∧ n₀ ∉ A⊢ ∀ (n : ℕ), n ∈ B ∧ n ∉ A ∨ n ∈ A ∧ n ∉ B → Nat.min (symmDiff B A) ≤ na:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h2:∀ (n : ℕ), n ∈ A ∧ n ∉ B ∨ n ∈ B ∧ n ∉ A → n₀ ≤ nthis:∀ ⦃A B : Set ℕ⦄,
f A = f B →
let n₀ := Nat.min (symmDiff A B);
n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ A → (∀ (n : ℕ), n ∈ A ∧ n ∉ B ∨ n ∈ B ∧ n ∉ A → n₀ ≤ n) → n₀ ∈ A ∧ n₀ ∉ B → Falseh:¬(n₀ ∈ A ∧ n₀ ∉ B)h1:n₀ ∈ B ∧ n₀ ∉ A⊢ Nat.min (symmDiff B A) ∈ B ∧ Nat.min (symmDiff B A) ∉ A a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h2:∀ (n : ℕ), n ∈ A ∧ n ∉ B ∨ n ∈ B ∧ n ∉ A → n₀ ≤ nthis:∀ ⦃A B : Set ℕ⦄,
f A = f B →
let n₀ := Nat.min (symmDiff A B);
n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ A → (∀ (n : ℕ), n ∈ A ∧ n ∉ B ∨ n ∈ B ∧ n ∉ A → n₀ ≤ n) → n₀ ∈ A ∧ n₀ ∉ B → Falseh:¬(n₀ ∈ A ∧ n₀ ∉ B)h1:n₀ ∈ B ∧ n₀ ∉ A⊢ Nat.min (symmDiff A B) ∈ B ∧ Nat.min (symmDiff A B) ∉ A a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h2:∀ (n : ℕ), n ∈ A ∧ n ∉ B ∨ n ∈ B ∧ n ∉ A → n₀ ≤ nthis:∀ ⦃A B : Set ℕ⦄,
f A = f B →
let n₀ := Nat.min (symmDiff A B);
n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ A → (∀ (n : ℕ), n ∈ A ∧ n ∉ B ∨ n ∈ B ∧ n ∉ A → n₀ ≤ n) → n₀ ∈ A ∧ n₀ ∉ B → Falseh:¬(n₀ ∈ A ∧ n₀ ∉ B)h1:n₀ ∈ B ∧ n₀ ∉ A⊢ Nat.min (symmDiff A B) ∈ B ∧ Nat.min (symmDiff A B) ∉ A ∨ Nat.min (symmDiff A B) ∈ A ∧ Nat.min (symmDiff A B) ∉ Ba:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h2:∀ (n : ℕ), n ∈ A ∧ n ∉ B ∨ n ∈ B ∧ n ∉ A → n₀ ≤ nthis:∀ ⦃A B : Set ℕ⦄,
f A = f B →
let n₀ := Nat.min (symmDiff A B);
n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ A → (∀ (n : ℕ), n ∈ A ∧ n ∉ B ∨ n ∈ B ∧ n ∉ A → n₀ ≤ n) → n₀ ∈ A ∧ n₀ ∉ B → Falseh:¬(n₀ ∈ A ∧ n₀ ∉ B)h1:n₀ ∈ B ∧ n₀ ∉ A⊢ ∀ (n : ℕ), n ∈ B ∧ n ∉ A ∨ n ∈ A ∧ n ∉ B → Nat.min (symmDiff A B) ≤ na:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h2:∀ (n : ℕ), n ∈ A ∧ n ∉ B ∨ n ∈ B ∧ n ∉ A → n₀ ≤ nthis:∀ ⦃A B : Set ℕ⦄,
f A = f B →
let n₀ := Nat.min (symmDiff A B);
n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ A → (∀ (n : ℕ), n ∈ A ∧ n ∉ B ∨ n ∈ B ∧ n ∉ A → n₀ ≤ n) → n₀ ∈ A ∧ n₀ ∉ B → Falseh:¬(n₀ ∈ A ∧ n₀ ∉ B)h1:n₀ ∈ B ∧ n₀ ∉ A⊢ Nat.min (symmDiff A B) ∈ B ∧ Nat.min (symmDiff A B) ∉ A All goals completed! 🐙
replace h2 {n:ℕ} (hn: n < n₀) : n ∈ A ↔ n ∈ B := ⊢ Uncountable ℝ All goals completed! 🐙
have : (0:ℝ) > 0 := calc
_ = f A - f B := a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ 0 = f A - f B All goals completed! 🐙
_ = ∑' n:A, a n - ∑' n:B, a n := rfl
_ = (∑' n:{n ∈ A|n ≤ n₀}, a n + ∑' n:{n ∈ A|n > n₀}, a n) -
(∑' n:{n ∈ B|n ≤ n₀}, a n + ∑' n:{n ∈ B|n > n₀}, a n) := a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ ∑' (n : ↑A), a ↑n - ∑' (n : ↑B), a ↑n =
∑' (n : ↑{n | n ∈ A ∧ n ≤ n₀}), a ↑n + ∑' (n : ↑{n | n ∈ A ∧ n > n₀}), a ↑n -
(∑' (n : ↑{n | n ∈ B ∧ n ≤ n₀}), a ↑n + ∑' (n : ↑{n | n ∈ B ∧ n > n₀}), a ↑n)
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ ∑' (n : ↑A), a ↑n = ∑' (n : ↑{n | n ∈ A ∧ n ≤ n₀}), a ↑n + ∑' (n : ↑{n | n ∈ A ∧ n > n₀}), a ↑na:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ ∑' (n : ↑B), a ↑n = ∑' (n : ↑{n | n ∈ B ∧ n ≤ n₀}), a ↑n + ∑' (n : ↑{n | n ∈ B ∧ n > n₀}), a ↑n; all_goals a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ ∑' (n : ↑B), a ↑n = ∑' (n : ↑{n | n ∈ B ∧ n ≤ n₀}), a ↑n + ∑' (n : ↑{n | n ∈ B ∧ n > n₀}), a ↑n
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ B = {n | n ∈ B ∧ n ≤ n₀} ∪ {n | n ∈ B ∧ n > n₀}a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ ∀ (n : ℕ), n ∉ {n | n ∈ B ∧ n ≤ n₀} ∩ {n | n ∈ B ∧ n > n₀}
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ B = {n | n ∈ B ∧ n ≤ n₀} ∪ {n | n ∈ B ∧ n > n₀} a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)n:ℕ⊢ n ∈ B ↔ n ∈ {n | n ∈ B ∧ n ≤ n₀} ∪ {n | n ∈ B ∧ n > n₀}; a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)n:ℕ⊢ n ∈ B ↔ n ∈ B ∧ n ≤ n₀ ∨ n ∈ B ∧ n₀ < n; All goals completed! 🐙
intro n a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)n:ℕhn:n ∈ {n | n ∈ B ∧ n ≤ n₀} ∩ {n | n ∈ B ∧ n > n₀}⊢ False; a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)n:ℕhn:(n ∈ B ∧ n ≤ n₀) ∧ n ∈ B ∧ n₀ < n⊢ False; All goals completed! 🐙
}
_ = ((∑' n:{n ∈ A|n < n₀}, a n + ∑' n:{n ∈ A|n = n₀}, a n) + ∑' n:{n ∈ A|n > n₀}, a n) -
((∑' n:{n ∈ B|n < n₀}, a n + ∑' n:{n ∈ B|n = n₀}, a n) + ∑' n:{n ∈ B|n > n₀}, a n) := a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ ∑' (n : ↑{n | n ∈ A ∧ n ≤ n₀}), a ↑n + ∑' (n : ↑{n | n ∈ A ∧ n > n₀}), a ↑n -
(∑' (n : ↑{n | n ∈ B ∧ n ≤ n₀}), a ↑n + ∑' (n : ↑{n | n ∈ B ∧ n > n₀}), a ↑n) =
∑' (n : ↑{n | n ∈ A ∧ n < n₀}), a ↑n + ∑' (n : ↑{n | n ∈ A ∧ n = n₀}), a ↑n + ∑' (n : ↑{n | n ∈ A ∧ n > n₀}), a ↑n -
(∑' (n : ↑{n | n ∈ B ∧ n < n₀}), a ↑n + ∑' (n : ↑{n | n ∈ B ∧ n = n₀}), a ↑n + ∑' (n : ↑{n | n ∈ B ∧ n > n₀}), a ↑n)
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ ∑' (n : ↑{n | n ∈ A ∧ n ≤ n₀}), a ↑n = ∑' (n : ↑{n | n ∈ A ∧ n < n₀}), a ↑n + ∑' (n : ↑{n | n ∈ A ∧ n = n₀}), a ↑na:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ ∑' (n : ↑{n | n ∈ B ∧ n ≤ n₀}), a ↑n = ∑' (n : ↑{n | n ∈ B ∧ n < n₀}), a ↑n + ∑' (n : ↑{n | n ∈ B ∧ n = n₀}), a ↑n; all_goals a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ ∑' (n : ↑{n | n ∈ B ∧ n ≤ n₀}), a ↑n = ∑' (n : ↑{n | n ∈ B ∧ n < n₀}), a ↑n + ∑' (n : ↑{n | n ∈ B ∧ n = n₀}), a ↑n
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ {n | n ∈ B ∧ n ≤ n₀} = {n | n ∈ B ∧ n < n₀} ∪ {n | n ∈ B ∧ n = n₀}a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ ∀ (n : ℕ), n ∉ {n | n ∈ B ∧ n < n₀} ∩ {n | n ∈ B ∧ n = n₀}
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ {n | n ∈ B ∧ n ≤ n₀} = {n | n ∈ B ∧ n < n₀} ∪ {n | n ∈ B ∧ n = n₀} a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)n:ℕ⊢ n ∈ {n | n ∈ B ∧ n ≤ n₀} ↔ n ∈ {n | n ∈ B ∧ n < n₀} ∪ {n | n ∈ B ∧ n = n₀}; All goals completed! 🐙
intro n a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)n:ℕhn:n ∈ {n | n ∈ B ∧ n < n₀} ∩ {n | n ∈ B ∧ n = n₀}⊢ False; a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)n:ℕhn:(n ∈ B ∧ n < n₀) ∧ n ∈ B ∧ n = n₀⊢ False; All goals completed! 🐙
}
_ = ((∑' n:{n ∈ A|n < n₀}, a n + a n₀) + ∑' n:{n ∈ A|n > n₀}, a n) -
((∑' n:{n ∈ B|n < n₀}, a n + 0) + ∑' n:{n ∈ B|n > n₀}, a n) := a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ ∑' (n : ↑{n | n ∈ A ∧ n < n₀}), a ↑n + ∑' (n : ↑{n | n ∈ A ∧ n = n₀}), a ↑n + ∑' (n : ↑{n | n ∈ A ∧ n > n₀}), a ↑n -
(∑' (n : ↑{n | n ∈ B ∧ n < n₀}), a ↑n + ∑' (n : ↑{n | n ∈ B ∧ n = n₀}), a ↑n +
∑' (n : ↑{n | n ∈ B ∧ n > n₀}), a ↑n) =
∑' (n : ↑{n | n ∈ A ∧ n < n₀}), a ↑n + a n₀ + ∑' (n : ↑{n | n ∈ A ∧ n > n₀}), a ↑n -
(∑' (n : ↑{n | n ∈ B ∧ n < n₀}), a ↑n + 0 + ∑' (n : ↑{n | n ∈ B ∧ n > n₀}), a ↑n)
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ ∑' (n : ↑{n | n ∈ A ∧ n = n₀}), a ↑n = a n₀a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ ∑' (n : ↑{n | n ∈ B ∧ n = n₀}), a ↑n = 0
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ ∑' (n : ↑{n | n ∈ A ∧ n = n₀}), a ↑n = a n₀ calc
_ = ∑' n:({n₀}:Set ℕ), a n := a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ ∑' (n : ↑{n | n ∈ A ∧ n = n₀}), a ↑n = ∑' (n : ↑{n₀}), a ↑n a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ {n | n ∈ A ∧ n = n₀} = {n₀}; a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)n:ℕ⊢ n ∈ {n | n ∈ A ∧ n = n₀} ↔ n ∈ {n₀}; a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)n:ℕ⊢ n = n₀ → n ∈ A; All goals completed! 🐙
_ = _ := a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ ∑' (n : ↑{n₀}), a ↑n = a n₀ All goals completed! 🐙
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ ∑' (n : ↑{n | n ∈ B ∧ n = n₀}), a ↑n = 0 calc
_ = ∑' n:(∅:Set ℕ), a n := a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ ∑' (n : ↑{n | n ∈ B ∧ n = n₀}), a ↑n = ∑' (n : ↑∅), a ↑n a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ {n | n ∈ B ∧ n = n₀} = ∅; a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)n:ℕ⊢ n ∈ {n | n ∈ B ∧ n = n₀} ↔ n ∈ ∅; a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)n:ℕ⊢ n ∈ B → ¬n = n₀; All goals completed! 🐙
_ = _ := a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ ∑' (n : ↑∅), a ↑n = 0 All goals completed! 🐙
_ = (∑' n:{n ∈ A|n < n₀}, a n - ∑' n:{n ∈ B|n < n₀}, a n) + a n₀ +
∑' n:{n ∈ A|n > n₀}, a n - ∑' n:{n ∈ B|n > n₀}, a n := a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ ∑' (n : ↑{n | n ∈ A ∧ n < n₀}), a ↑n + a n₀ + ∑' (n : ↑{n | n ∈ A ∧ n > n₀}), a ↑n -
(∑' (n : ↑{n | n ∈ B ∧ n < n₀}), a ↑n + 0 + ∑' (n : ↑{n | n ∈ B ∧ n > n₀}), a ↑n) =
∑' (n : ↑{n | n ∈ A ∧ n < n₀}), a ↑n - ∑' (n : ↑{n | n ∈ B ∧ n < n₀}), a ↑n + a n₀ +
∑' (n : ↑{n | n ∈ A ∧ n > n₀}), a ↑n -
∑' (n : ↑{n | n ∈ B ∧ n > n₀}), a ↑n All goals completed! 🐙
_ = 0 + a n₀ + ∑' n:{n ∈ A|n > n₀}, a n - ∑' n:{n ∈ B|n > n₀}, a n := a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ ∑' (n : ↑{n | n ∈ A ∧ n < n₀}), a ↑n - ∑' (n : ↑{n | n ∈ B ∧ n < n₀}), a ↑n + a n₀ +
∑' (n : ↑{n | n ∈ A ∧ n > n₀}), a ↑n -
∑' (n : ↑{n | n ∈ B ∧ n > n₀}), a ↑n =
0 + a n₀ + ∑' (n : ↑{n | n ∈ A ∧ n > n₀}), a ↑n - ∑' (n : ↑{n | n ∈ B ∧ n > n₀}), a ↑n
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ ∑' (n : ↑{n | n ∈ A ∧ n < n₀}), a ↑n - ∑' (n : ↑{n | n ∈ B ∧ n < n₀}), a ↑n = 0; a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ ∑' (n : ↑{n | n ∈ A ∧ n < n₀}), a ↑n = ∑' (n : ↑{n | n ∈ B ∧ n < n₀}), a ↑n; a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ {n | n ∈ A ∧ n < n₀} = {n | n ∈ B ∧ n < n₀}; All goals completed! 🐙
_ ≥ 0 + a n₀ + 0 - ∑' n:{n|n > n₀}, a n := a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ 0 + a n₀ + ∑' (n : ↑{n | n ∈ A ∧ n > n₀}), a ↑n - ∑' (n : ↑{n | n ∈ B ∧ n > n₀}), a ↑n ≥
0 + a n₀ + 0 - ∑' (n : ↑{n | n > n₀}), a ↑n
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ 0 ≤ ∑' (n : ↑{n | n ∈ A ∧ n > n₀}), a ↑na:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ ∑' (n : ↑{n | n ∈ B ∧ n > n₀}), a ↑n ≤ ∑' (n : ↑{n | n > n₀}), a ↑n; a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ ∑' (n : ↑{n | n ∈ B ∧ n > n₀}), a ↑n ≤ ∑' (n : ↑{n | n > n₀}), a ↑n
calc
_ = ∑' (n : {n ∈ B|n > n₀}), a n + ∑' (n : {n ∉ B|n > n₀}), a n := a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ ∑' (n : ↑{n | n > n₀}), a ↑n = ∑' (n : ↑{n | n ∈ B ∧ n > n₀}), a ↑n + ∑' (n : ↑{n | n ∉ B ∧ n > n₀}), a ↑n
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ {n | n > n₀} = {n | n ∈ B ∧ n > n₀} ∪ {n | n ∉ B ∧ n > n₀}a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ ∀ (n : ℕ), n ∉ {n | n ∈ B ∧ n > n₀} ∩ {n | n ∉ B ∧ n > n₀}
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ {n | n > n₀} = {n | n ∈ B ∧ n > n₀} ∪ {n | n ∉ B ∧ n > n₀} a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)n:ℕ⊢ n ∈ {n | n > n₀} ↔ n ∈ {n | n ∈ B ∧ n > n₀} ∪ {n | n ∉ B ∧ n > n₀}; a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)n:ℕ⊢ n₀ < n ↔ n ∈ B ∧ n₀ < n ∨ n ∉ B ∧ n₀ < n; All goals completed! 🐙
intro n a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)n:ℕhn:n ∈ {n | n ∈ B ∧ n > n₀} ∩ {n | n ∉ B ∧ n > n₀}⊢ False; a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)n:ℕhn:(n ∈ B ∧ n₀ < n) ∧ n ∉ B ∧ n₀ < n⊢ False; All goals completed! 🐙
_ ≥ ∑' (n : {n ∈ B|n > n₀}), a n + 0 := a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ ∑' (n : ↑{n | n ∈ B ∧ n > n₀}), a ↑n + ∑' (n : ↑{n | n ∉ B ∧ n > n₀}), a ↑n ≥ ∑' (n : ↑{n | n ∈ B ∧ n > n₀}), a ↑n + 0 a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ 0 ≤ ∑' (n : ↑{n | n ∉ B ∧ n > n₀}), a ↑n; All goals completed! 🐙
_ = _ := a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ ∑' (n : ↑{n | n ∈ B ∧ n > n₀}), a ↑n + 0 = ∑' (n : ↑{n | n ∈ B ∧ n > n₀}), a ↑n All goals completed! 🐙
_ = 0 + (10:ℝ)^(-(n₀:ℝ)) + 0 - (1 / (9:ℝ)) * (10:ℝ)^(-(n₀:ℝ)) := a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ 0 + a n₀ + 0 - ∑' (n : ↑{n | n > n₀}), a ↑n = 0 + 10 ^ (-↑n₀) + 0 - 1 / 9 * 10 ^ (-↑n₀)
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ ∑' (n : ↑{n | n > n₀}), a ↑n = 1 / 9 * 10 ^ (-↑n₀)
set ι : ℕ → {n | n > n₀} := fun j ↦ ⟨ j+(n₀+1), a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)j:ℕ⊢ j + (n₀ + 1) ∈ {n | n > n₀} a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)j:ℕ⊢ n₀ < j + (n₀ + 1); All goals completed! 🐙 ⟩
have hι : Function.Bijective ι := a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ 0 + a n₀ + 0 - ∑' (n : ↑{n | n > n₀}), a ↑n = 0 + 10 ^ (-↑n₀) + 0 - 1 / 9 * 10 ^ (-↑n₀)
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)ι:ℕ → ↑{n | n > n₀} := fun j ↦ ⟨j + (n₀ + 1), ⋯⟩⊢ Function.Injective ιa:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)ι:ℕ → ↑{n | n > n₀} := fun j ↦ ⟨j + (n₀ + 1), ⋯⟩⊢ Function.Surjective ι
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)ι:ℕ → ↑{n | n > n₀} := fun j ↦ ⟨j + (n₀ + 1), ⋯⟩⊢ Function.Injective ι intro j a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)ι:ℕ → ↑{n | n > n₀} := fun j ↦ ⟨j + (n₀ + 1), ⋯⟩j:ℕk:ℕ⊢ ι j = ι k → j = k a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)ι:ℕ → ↑{n | n > n₀} := fun j ↦ ⟨j + (n₀ + 1), ⋯⟩j:ℕk:ℕhjk:ι j = ι k⊢ j = k; All goals completed! 🐙
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)ι:ℕ → ↑{n | n > n₀} := fun j ↦ ⟨j + (n₀ + 1), ⋯⟩n:ℕhn:n ∈ {n | n > n₀}⊢ ∃ a, ι a = ⟨n, hn⟩; a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)ι:ℕ → ↑{n | n > n₀} := fun j ↦ ⟨j + (n₀ + 1), ⋯⟩n:ℕhn:n₀ < n⊢ ∃ a, a + (n₀ + 1) = n; a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)ι:ℕ → ↑{n | n > n₀} := fun j ↦ ⟨j + (n₀ + 1), ⋯⟩n:ℕhn:n₀ < n⊢ n - n₀ - 1 + (n₀ + 1) = n; All goals completed! 🐙
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)ι:ℕ → ↑{n | n > n₀} := fun j ↦ ⟨j + (n₀ + 1), ⋯⟩hι:Function.Bijective ι⊢ ∑' (c : ℕ), a ↑((Equiv.ofBijective ι hι) c) = 1 / 9 * 10 ^ (-↑n₀)
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)ι:ℕ → ↑{n | n > n₀} := fun j ↦ ⟨j + (n₀ + 1), ⋯⟩hι:Function.Bijective ι⊢ ∑' (c : ℕ), (10 ^ ↑((Equiv.ofBijective (fun j ↦ ⟨j + (n₀ + 1), ⋯⟩) ⋯) c))⁻¹ = 9⁻¹ * (10 ^ n₀)⁻¹
calc
_ = ∑' j:ℕ, (10:ℝ)^(-1-n₀:ℝ) * (1/(10:ℝ))^j := a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)ι:ℕ → ↑{n | n > n₀} := fun j ↦ ⟨j + (n₀ + 1), ⋯⟩hι:Function.Bijective ι⊢ ∑' (c : ℕ), (10 ^ ↑((Equiv.ofBijective (fun j ↦ ⟨j + (n₀ + 1), ⋯⟩) ⋯) c))⁻¹ = ∑' (j : ℕ), 10 ^ (-1 - ↑n₀) * (1 / 10) ^ j
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)ι:ℕ → ↑{n | n > n₀} := fun j ↦ ⟨j + (n₀ + 1), ⋯⟩hι:Function.Bijective ι⊢ ∀ (b : ℕ), (10 ^ ↑((Equiv.ofBijective (fun j ↦ ⟨j + (n₀ + 1), ⋯⟩) ⋯) b))⁻¹ = 10 ^ (-1 - ↑n₀) * (1 / 10) ^ b; a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)ι:ℕ → ↑{n | n > n₀} := fun j ↦ ⟨j + (n₀ + 1), ⋯⟩hι:Function.Bijective ιj:ℕ⊢ (10 ^ ↑((Equiv.ofBijective (fun j ↦ ⟨j + (n₀ + 1), ⋯⟩) ⋯) j))⁻¹ = 10 ^ (-1 - ↑n₀) * (1 / 10) ^ j
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)ι:ℕ → ↑{n | n > n₀} := fun j ↦ ⟨j + (n₀ + 1), ⋯⟩hι:Function.Bijective ιj:ℕ⊢ (10 ^ (j + (n₀ + 1)))⁻¹ = 10 ^ (-1 - ↑n₀) * (1 / 10) ^ j
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)ι:ℕ → ↑{n | n > n₀} := fun j ↦ ⟨j + (n₀ + 1), ⋯⟩hι:Function.Bijective ιj:ℕ⊢ (10 ^ j * (10 ^ n₀ * 10 ^ 1))⁻¹ = 10⁻¹ / 10 ^ n₀ * (1 / 10) ^ ja:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)ι:ℕ → ↑{n | n > n₀} := fun j ↦ ⟨j + (n₀ + 1), ⋯⟩hι:Function.Bijective ιj:ℕ⊢ 0 ≤ 10a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)ι:ℕ → ↑{n | n > n₀} := fun j ↦ ⟨j + (n₀ + 1), ⋯⟩hι:Function.Bijective ιj:ℕ⊢ 0 < 10 a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)ι:ℕ → ↑{n | n > n₀} := fun j ↦ ⟨j + (n₀ + 1), ⋯⟩hι:Function.Bijective ιj:ℕ⊢ (10 ^ j * (10 ^ n₀ * 10 ^ 1))⁻¹ = 10⁻¹ / 10 ^ n₀ * (1 / 10) ^ ja:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)ι:ℕ → ↑{n | n > n₀} := fun j ↦ ⟨j + (n₀ + 1), ⋯⟩hι:Function.Bijective ιj:ℕ⊢ 0 ≤ 10a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)ι:ℕ → ↑{n | n > n₀} := fun j ↦ ⟨j + (n₀ + 1), ⋯⟩hι:Function.Bijective ιj:ℕ⊢ 0 < 10 try All goals completed! 🐙
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)ι:ℕ → ↑{n | n > n₀} := fun j ↦ ⟨j + (n₀ + 1), ⋯⟩hι:Function.Bijective ιj:ℕ⊢ 10⁻¹ * (10 ^ n₀)⁻¹ = 10⁻¹ / 10 ^ n₀; All goals completed! 🐙
_ = (10:ℝ)^(-1-n₀:ℝ) * ∑' j:ℕ, (1/(10:ℝ))^j := tsum_mul_left
_ = _ := a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)ι:ℕ → ↑{n | n > n₀} := fun j ↦ ⟨j + (n₀ + 1), ⋯⟩hι:Function.Bijective ι⊢ 10 ^ (-1 - ↑n₀) * ∑' (j : ℕ), (1 / 10) ^ j = 9⁻¹ * (10 ^ n₀)⁻¹
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)ι:ℕ → ↑{n | n > n₀} := fun j ↦ ⟨j + (n₀ + 1), ⋯⟩hι:Function.Bijective ι⊢ (10 ^ n₀)⁻¹ * 10 ^ (-1) * (1 - 1 / 10)⁻¹ = 9⁻¹ * (10 ^ n₀)⁻¹a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)ι:ℕ → ↑{n | n > n₀} := fun j ↦ ⟨j + (n₀ + 1), ⋯⟩hι:Function.Bijective ι⊢ 0 ≤ 10a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)ι:ℕ → ↑{n | n > n₀} := fun j ↦ ⟨j + (n₀ + 1), ⋯⟩hι:Function.Bijective ι⊢ 0 < 10a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)ι:ℕ → ↑{n | n > n₀} := fun j ↦ ⟨j + (n₀ + 1), ⋯⟩hι:Function.Bijective ι⊢ -1 - ↑n₀ = -↑n₀ + -1a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)ι:ℕ → ↑{n | n > n₀} := fun j ↦ ⟨j + (n₀ + 1), ⋯⟩hι:Function.Bijective ι⊢ 0 ≤ 1 / 10a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)ι:ℕ → ↑{n | n > n₀} := fun j ↦ ⟨j + (n₀ + 1), ⋯⟩hι:Function.Bijective ι⊢ 1 / 10 < 1 a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)ι:ℕ → ↑{n | n > n₀} := fun j ↦ ⟨j + (n₀ + 1), ⋯⟩hι:Function.Bijective ι⊢ (10 ^ n₀)⁻¹ * 10 ^ (-1) * (1 - 1 / 10)⁻¹ = 9⁻¹ * (10 ^ n₀)⁻¹a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)ι:ℕ → ↑{n | n > n₀} := fun j ↦ ⟨j + (n₀ + 1), ⋯⟩hι:Function.Bijective ι⊢ 0 ≤ 10a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)ι:ℕ → ↑{n | n > n₀} := fun j ↦ ⟨j + (n₀ + 1), ⋯⟩hι:Function.Bijective ι⊢ 0 < 10a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)ι:ℕ → ↑{n | n > n₀} := fun j ↦ ⟨j + (n₀ + 1), ⋯⟩hι:Function.Bijective ι⊢ -1 - ↑n₀ = -↑n₀ + -1a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)ι:ℕ → ↑{n | n > n₀} := fun j ↦ ⟨j + (n₀ + 1), ⋯⟩hι:Function.Bijective ι⊢ 0 ≤ 1 / 10a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)ι:ℕ → ↑{n | n > n₀} := fun j ↦ ⟨j + (n₀ + 1), ⋯⟩hι:Function.Bijective ι⊢ 1 / 10 < 1 try a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)ι:ℕ → ↑{n | n > n₀} := fun j ↦ ⟨j + (n₀ + 1), ⋯⟩hι:Function.Bijective ι⊢ 1 / 10 < 1
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)ι:ℕ → ↑{n | n > n₀} := fun j ↦ ⟨j + (n₀ + 1), ⋯⟩hι:Function.Bijective ι⊢ -1 - ↑n₀ = -↑n₀ + -1a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)ι:ℕ → ↑{n | n > n₀} := fun j ↦ ⟨j + (n₀ + 1), ⋯⟩hι:Function.Bijective ι⊢ 1 / 10 < 1; a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)ι:ℕ → ↑{n | n > n₀} := fun j ↦ ⟨j + (n₀ + 1), ⋯⟩hι:Function.Bijective ι⊢ 1 / 10 < 1; All goals completed! 🐙
_ = (8 / (9:ℝ)) * (10:ℝ)^(-(n₀:ℝ)) := a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ 0 + 10 ^ (-↑n₀) + 0 - 1 / 9 * 10 ^ (-↑n₀) = 8 / 9 * 10 ^ (-↑n₀) All goals completed! 🐙
_ > 0 := a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nA:Set ℕB:Set ℕhAB:f A = f Bn₀:ℕ := Nat.min (symmDiff A B)h1:n₀ ∈ A ∧ n₀ ∉ B ∨ n₀ ∈ B ∧ n₀ ∉ Ah:n₀ ∈ A ∧ n₀ ∉ Bh2:∀ {n : ℕ}, n < n₀ → (n ∈ A ↔ n ∈ B)⊢ 8 / 9 * 10 ^ (-↑n₀) > 0 All goals completed! 🐙
All goals completed! 🐙
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nthis:EqualCard (Set ℕ) ↑(Set.range f)⊢ Uncountable ℝ
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nthis:Uncountable ↑(Set.range f)⊢ Uncountable ℝ
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nthis:¬Uncountable ℝ⊢ ¬Uncountable ↑(Set.range f)
a:ℕ → ℝ := fun n ↦ 10 ^ (-↑n)f:Set ℕ → ℝ := fun A ↦ ∑' (n : ↑A), a ↑nhsummable:∀ (A : Set ℕ), Summable fun n ↦ a ↑nh_decomp:∀ {A B C : Set ℕ}, C = A ∪ B → (∀ (n : ℕ), n ∉ A ∩ B) → ∑' (n : ↑C), a ↑n = ∑' (n : ↑A), a ↑n + ∑' (n : ↑B), a ↑nh_nonneg:∀ (A : Set ℕ), ∑' (n : ↑A), a ↑n ≥ 0h_congr:∀ {A B : Set ℕ}, A = B → ∑' (n : ↑A), a ↑n = ∑' (n : ↑B), a ↑nthis:Countable ℝ⊢ Countable ↑(Set.range f)
All goals completed! 🐙/-- Exercise 8.3.1 -/
example {X:Type} [Finite X] : Nat.card (Set X) = 2 ^ Nat.card X := X:Typeinst✝:Finite X⊢ Nat.card (Set X) = 2 ^ Nat.card X
All goals completed! 🐙
Exercise 8.3.2. Some subtle type changes due to how sets are implemented in Mathlib. Also we shift the sequence D by one so that we can work in Set A rather than Set B.
open Classical intheorem Schroder_Bernstein_lemma {X: Type} {A B C: Set X} (hAB: A ⊆ B) (hBC: B ⊆ C) (f: C ↪ A) :
let D : ℕ → Set A := Nat.rec ((f.image ∘ ((B.embeddingOfSubset _ hBC).image)) {x:B | ↑x ∉ A}) (fun _ ↦ (f.image ∘ ((B.embeddingOfSubset _ hBC).image) ∘ (A.embeddingOfSubset _ hAB).image))
Set.univ.PairwiseDisjoint D ∧
let g : A → B := fun x ↦ if h: x ∈ ⋃ n, D n ∧ ∃ y:B, f ⟨↑y, hBC y.property⟩ = x then h.2.choose else ⟨ ↑x, hAB x.property ⟩
Function.Bijective g
:= X:TypeA:Set XB:Set XC:Set XhAB:A ⊆ BhBC:B ⊆ Cf:↑C ↪ ↑A⊢ let D := fun t ↦
Nat.rec ((⇑f.image ∘ ⇑(B.embeddingOfSubset C hBC).image) {x | ↑x ∉ A})
(fun x ↦ ⇑f.image ∘ ⇑(B.embeddingOfSubset C hBC).image ∘ ⇑(A.embeddingOfSubset B hAB).image) t;
Set.univ.PairwiseDisjoint D ∧
let g := fun x ↦ if h : x ∈ ⋃ n, D n ∧ ∃ y, f ⟨↑y, ⋯⟩ = x then ⋯.choose else ⟨↑x, ⋯⟩;
Function.Bijective g
All goals completed! 🐙abbrev LeCard (X Y: Type) : Prop := ∃ f: X → Y, Function.Injective fExercise 8.3.3
theorem Schroder_Bernstein {X Y:Type} (hXY : LeCard X Y) (hYX : LeCard Y X) : EqualCard X Y := X:TypeY:TypehXY:LeCard X YhYX:LeCard Y X⊢ EqualCard X Y
All goals completed! 🐙abbrev LtCard (X Y: Type) : Prop := LeCard X Y ∧ ¬ EqualCard X Y/-- Exercise 8.3.4 -/
example {X:Type} : LtCard X (Set X) := X:Type⊢ LtCard X (Set X) All goals completed! 🐙example {A B C: Type} (hAB: LtCard A B) (hBC: LtCard B C) :
LtCard A C := A:TypeB:TypeC:TypehAB:LtCard A BhBC:LtCard B C⊢ LtCard A C
All goals completed! 🐙abbrev CardOrder : Preorder Type := {
le := LeCard
lt := LtCard
le_refl := ⊢ ∀ (a : Type), LeCard a a
All goals completed! 🐙
le_trans := ⊢ ∀ (a b c : Type), LeCard a b → LeCard b c → LeCard a c
All goals completed! 🐙
lt_iff_le_not_ge := ⊢ ∀ (a b : Type), LtCard a b ↔ LeCard a b ∧ ¬LeCard b a
All goals completed! 🐙
}/-- Exercise 8.3.5 -/
example (X:Type) : ¬ CountablyInfinite (Set X) := X:Type⊢ ¬CountablyInfinite (Set X)
All goals completed! 🐙end Chapter8