Built with Alectryon, running Lean4 v4.13.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+βCtrl+β to navigate, Ctrl+π±οΈ to focus. On Mac, use β instead of Ctrl.
/--β€ is countable-/lemma Z_countable : countable (univ : Set β€) :=
Goals accomplished!π
countable univ
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€
countable univ
countable univ
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€
countable univ
Goals accomplished!π
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€
SurjOn f univ univ
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€
SurjOn f univ univ
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€
SurjOn f univ univ
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ
z β f '' univ
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€
SurjOn f univ univ
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z
pos
z β f '' univ
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: Β¬0< z
z β f '' univ
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€
SurjOn f univ univ
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z
pos
z β f '' univ
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z
pos
z β f '' univ
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: Β¬0< z
z β f '' univ
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z n:= 2* (z -1).toNat +1: β
pos
z β f '' univ
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z
pos
z β f '' univ
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z n:= 2* (z -1).toNat +1: β
pos
z β f '' univ
Goals accomplished!π
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z n:= 2* (z -1).toNat +1: β
pos
z β f '' univ
Goals accomplished!π
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z
pos
z β f '' univ
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z n:= 2* (z -1).toNat +1: β odd_n: Odd n
h
n β univ β§ f n = z
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z
pos
z β f '' univ
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z n:= 2* (z -1).toNat +1: β odd_n: Odd n
h
f n = z
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z
pos
z β f '' univ
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z n:= 2* (z -1).toNat +1: β odd_n: Odd n
h
f n = z
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z n:= 2* (z -1).toNat +1: β odd_n: Odd n
h
f n = z
Goals accomplished!π
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z n:= 2* (z -1).toNat +1: β odd_n: Odd n
h
(if h : Even n then-(βn /2) else (βn -1) /2+1) = z
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z
pos
z β f '' univ
[Meta.Tactic.simp.rewrite] dif_pos:1000, if h : Even n then-(βn /2) else (βn -1) /2+1==>-(βn /2)
[Meta.Tactic.simp.rewrite] dif_neg:1000, if h : Even n then-(βn /2) else (βn -1) /2+1==> (βn -1) /2+1
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z n:= 2* (z -1).toNat +1: β odd_n: Odd n hβ: Even n
h.isTrue
-(βn /2) = z
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z n:= 2* (z -1).toNat +1: β odd_n: Odd n hβ: Β¬Even n
(βn -1) /2+1= z
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z
pos
z β f '' univ
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z n:= 2* (z -1).toNat +1: β odd_n: Odd n hβ: Even n
h.isTrue
-(βn /2) = z
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z n:= 2* (z -1).toNat +1: β odd_n: Odd n hβ: Β¬Even n
(βn -1) /2+1= z
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z n:= 2* (z -1).toNat +1: β odd_n: Odd n h_if: Even n
False
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z n:= 2* (z -1).toNat +1: β odd_n: Odd n h_if: Even n
-(βn /2) = z
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z n:= 2* (z -1).toNat +1: β odd_n: Odd n h_if: Even n
False
Warning: `Nat.odd_iff_not_even` has been deprecated, use `Nat.not_even_iff_odd` instead
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z n:= 2* (z -1).toNat +1: β odd_n: Odd n h_if: Even n
False
Goals accomplished!π
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z
pos
z β f '' univ
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z n:= 2* (z -1).toNat +1: β odd_n: Odd n hβ: Β¬Even n
h.isFalse
(βn -1) /2+1= z
Goals accomplished!π
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z n:= 2* (z -1).toNat +1: β odd_n: Odd n hβ: Β¬Even n
βn =2* (z -1) +1
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z n:= 2* (z -1).toNat +1: β odd_n: Odd n hβ: Β¬Even n
βn =2* (z -1) +1
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z n:= 2* (z -1).toNat +1: β odd_n: Odd n hβ: Β¬Even n
βn =2* (z -1) +1
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z n:= 2* (z -1).toNat +1: β odd_n: Odd n hβ: Β¬Even n coe_tmp: β(z -1).toNat = z -1
βn =2* (z -1) +1
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z n:= 2* (z -1).toNat +1: β odd_n: Odd n hβ: Β¬Even n
βn =2* (z -1) +1
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z n:= 2* (z -1).toNat +1: β odd_n: Odd n hβ: Β¬Even n coe_tmp: β(z -1).toNat = z -1
βn =2* (z -1) +1
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z n:= 2* (z -1).toNat +1: β odd_n: Odd n hβ: Β¬Even n coe_tmp: β(z -1).toNat = z -1
βn =2*β(z -1).toNat +1
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z n:= 2* (z -1).toNat +1: β odd_n: Odd n hβ: Β¬Even n coe_tmp: β(z -1).toNat = z -1
βn =2*β(z -1).toNat +1
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z n:= 2* (z -1).toNat +1: β odd_n: Odd n hβ: Β¬Even n
βn =2* (z -1) +1
Goals accomplished!π
Goals accomplished!π
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z
pos
z β f '' univ
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z n:= 2* (z -1).toNat +1: β odd_n: Odd n hβ: Β¬Even n coe: βn =2* (z -1) +1
h.isFalse
(βn -1) /2+1= z
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z n:= 2* (z -1).toNat +1: β odd_n: Odd n hβ: Β¬Even n coe: βn =2* (z -1) +1
h.isFalse
(2* (z -1) +1-1) /2+1= z
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z n:= 2* (z -1).toNat +1: β odd_n: Odd n hβ: Β¬Even n coe: βn =2* (z -1) +1
h.isFalse
(2* (z -1) +1-1) /2+1= z
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z
pos
z β f '' univ
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z n:= 2* (z -1).toNat +1: β odd_n: Odd n hβ: Β¬Even n coe: βn =2* (z -1) +1
h.isFalse
(2* (z -1) +1-1) /2+1= z
Goals accomplished!π
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z n:= 2* (z -1).toNat +1: β odd_n: Odd n hβ: Β¬Even n coe: βn =2* (z -1) +1
(2* (z -1) +1-1) /2+1=2* (z -1) /2+1
[Meta.Tactic.simp.rewrite] add_sub_cancel_right:1000, 2* (z -1) +1-1==>2* (z -1)
[Meta.Tactic.simp.rewrite] ne_eq:1000, 2β 0==>Β¬2=0
[Meta.Tactic.simp.rewrite] OfNat.ofNat_ne_zero:1000, 2=0==> False
[Meta.Tactic.simp.rewrite] not_false_eq_true:1000, Β¬False ==> True
[Meta.Tactic.simp.rewrite] mul_div_cancel_leftβ:1000, 2* (z -1) /2==> z -1
[Meta.Tactic.simp.rewrite] sub_add_cancel:1000, z -1+1==> z
[Meta.Tactic.simp.rewrite] ne_eq:1000, 2β 0==>Β¬2=0
[Meta.Tactic.simp.rewrite] OfNat.ofNat_ne_zero:1000, 2=0==> False
[Meta.Tactic.simp.rewrite] not_false_eq_true:1000, Β¬False ==> True
[Meta.Tactic.simp.rewrite] mul_div_cancel_leftβ:1000, 2* (z -1) /2==> z -1
[Meta.Tactic.simp.rewrite] sub_add_cancel:1000, z -1+1==> z
[Meta.Tactic.simp.rewrite] eq_self:1000, z = z ==> True
Goals accomplished!π
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z n:= 2* (z -1).toNat +1: β odd_n: Odd n hβ: Β¬Even n coe: βn =2* (z -1) +1
h.isFalse
(2* (z -1) +1-1) /2+1= z
Goals accomplished!π
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z n:= 2* (z -1).toNat +1: β odd_n: Odd n hβ: Β¬Even n coe: βn =2* (z -1) +1
2* (z -1) /2+1= z -1+1
[Meta.Tactic.simp.rewrite] ne_eq:1000, 2β 0==>Β¬2=0
[Meta.Tactic.simp.rewrite] OfNat.ofNat_ne_zero:1000, 2=0==> False
[Meta.Tactic.simp.rewrite] not_false_eq_true:1000, Β¬False ==> True
[Meta.Tactic.simp.rewrite] mul_div_cancel_leftβ:1000, 2* (z -1) /2==> z -1
[Meta.Tactic.simp.rewrite] sub_add_cancel:1000, z -1+1==> z
[Meta.Tactic.simp.rewrite] sub_add_cancel:1000, z -1+1==> z
[Meta.Tactic.simp.rewrite] eq_self:1000, z = z ==> True
Goals accomplished!π
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z n:= 2* (z -1).toNat +1: β odd_n: Odd n hβ: Β¬Even n coe: βn =2* (z -1) +1
h.isFalse
(2* (z -1) +1-1) /2+1= z
Goals accomplished!π
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: 0< z n:= 2* (z -1).toNat +1: β odd_n: Odd n hβ: Β¬Even n coe: βn =2* (z -1) +1
z -1+1= z
[Meta.Tactic.simp.rewrite] sub_add_cancel:1000, z -1+1==> z
[Meta.Tactic.simp.rewrite] eq_self:1000, z = z ==> True
Goals accomplished!π
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€
SurjOn f univ univ
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: z β€0
neg
z β f '' univ
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€
SurjOn f univ univ
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: z β€0 n:= 2* (-z).toNat: β
neg
z β f '' univ
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€
SurjOn f univ univ
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: z β€0 n:= 2* (-z).toNat: β
neg
z β f '' univ
Goals accomplished!π
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: z β€0 n:= 2* (-z).toNat: β
Even n
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: z β€0 n:= 2* (-z).toNat: β
Even n
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: z β€0 n:= 2* (-z).toNat: β
Even n
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: z β€0 n:= 2* (-z).toNat: β
β r, n = r + r
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: z β€0 n:= 2* (-z).toNat: β
Even n
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: z β€0 n:= 2* (-z).toNat: β
h
n = (-z).toNat + (-z).toNat
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: z β€0 n:= 2* (-z).toNat: β
Even n
Goals accomplished!π
Goals accomplished!π
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€
SurjOn f univ univ
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: z β€0 n:= 2* (-z).toNat: β even_n: Even n
h
n β univ β§ f n = z
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€
SurjOn f univ univ
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: z β€0 n:= 2* (-z).toNat: β even_n: Even n
h
f n = z
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€
SurjOn f univ univ
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: z β€0 n:= 2* (-z).toNat: β even_n: Even n
h
f n = z
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: z β€0 n:= 2* (-z).toNat: β even_n: Even n
h
f n = z
Goals accomplished!π
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: z β€0 n:= 2* (-z).toNat: β even_n: Even n
h
(if h : Even n then-(βn /2) else (βn -1) /2+1) = z
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€
SurjOn f univ univ
[Meta.Tactic.simp.rewrite] dif_pos:1000, if h : Even n then-(βn /2) else (βn -1) /2+1==>-(βn /2)
[Meta.Tactic.simp.rewrite] dif_pos:1000, if h : Even n then-(βn /2) else (βn -1) /2+1==>-(βn /2)
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: z β€0 n:= 2* (-z).toNat: β even_n, hβ: Even n
h.isTrue
-(βn /2) = z
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: z β€0 n:= 2* (-z).toNat: β even_n: Even n hβ: Β¬Even n
-(βn /2) = z
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€
SurjOn f univ univ
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: z β€0 n:= 2* (-z).toNat: β even_n, hβ: Even n
h.isTrue
-(βn /2) = z
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: z β€0 n:= 2* (-z).toNat: β even_n, hβ: Even n
h.isTrue
-(βn /2) = z
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: z β€0 n:= 2* (-z).toNat: β even_n: Even n hβ: Β¬Even n
-(βn /2) = z
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: z β€0 n:= 2* (-z).toNat: β even_n, hβ: Even n coe: β(-z).toNat =-z
h.isTrue
-(βn /2) = z
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: z β€0 n:= 2* (-z).toNat: β even_n, hβ: Even n
h.isTrue
-(βn /2) = z
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: z β€0 n:= 2* (-z).toNat: β even_n, hβ: Even n coe: β(-z).toNat =-z m_z:= -z: β€
h.isTrue
-(βn /2) = z
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: z β€0 n:= 2* (-z).toNat: β even_n, hβ: Even n
h.isTrue
-(βn /2) = z
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: z β€0 n:= 2* (-z).toNat: β even_n, hβ: Even n coe: β(-z).toNat =-z m_z:= -z: β€
h.isTrue
-(βn /2) = z
Goals accomplished!π
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: z β€0 n:= 2* (-z).toNat: β even_n, hβ: Even n coe: β(-z).toNat =-z m_z:= -z: β€
-(βn /2) =-(2*β(-z).toNat /2)
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: z β€0 n:= 2* (-z).toNat: β even_n, hβ: Even n coe: β(-z).toNat =-z m_z:= -z: β€
-(βn /2) =-(2*β(-z).toNat /2)
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: z β€0 n:= 2* (-z).toNat: β even_n, hβ: Even n coe: β(-z).toNat =-z m_z:= -z: β€
-(βn /2) =-(2*β(-z).toNat /2)
Goals accomplished!π
Goals accomplished!π
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: z β€0 n:= 2* (-z).toNat: β even_n, hβ: Even n coe: β(-z).toNat =-z m_z:= -z: β€
h.isTrue
-(βn /2) = z
Goals accomplished!π
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: z β€0 n:= 2* (-z).toNat: β even_n, hβ: Even n coe: β(-z).toNat =-z m_z:= -z: β€
-(2*β(-z).toNat /2) =-(2* m_z /2)
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: z β€0 n:= 2* (-z).toNat: β even_n, hβ: Even n coe: β(-z).toNat =-z m_z:= -z: β€
-(2*β(-z).toNat /2) =-(2* m_z /2)
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: z β€0 n:= 2* (-z).toNat: β even_n, hβ: Even n coe: β(-z).toNat =-z m_z:= -z: β€
-(2*-z /2) =-(2* m_z /2)
Goals accomplished!π
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: z β€0 n:= 2* (-z).toNat: β even_n, hβ: Even n coe: β(-z).toNat =-z m_z:= -z: β€
h.isTrue
-(βn /2) = z
Goals accomplished!π
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: z β€0 n:= 2* (-z).toNat: β even_n, hβ: Even n coe: β(-z).toNat =-z m_z:= -z: β€
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: z β€0 n:= 2* (-z).toNat: β even_n, hβ: Even n coe: β(-z).toNat =-z m_z:= -z: β€
h.isTrue
-(βn /2) = z
Goals accomplished!π
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€ z: β€ aβ: z β univ h: z β€0 n:= 2* (-z).toNat: β even_n, hβ: Even n coe: β(-z).toNat =-z m_z:= -z: β€
--z = z
[Meta.Tactic.simp.rewrite] neg_neg:1000, --z ==> z
[Meta.Tactic.simp.rewrite] eq_self:1000, z = z ==> True
Goals accomplished!π
f:= fun n =>if h : Even n then-(βn /2) else (βn -1) /2+1: β β β€
SurjOn f univ univ
Goals accomplished!π
Goals accomplished!π
countable univ
Goals accomplished!π
/--Let E a set. E is countable iff it exists a surjection from a countable set A to E.-/lemma countable_trans {u : Type} {E : Set u} : countable E β (β (v : Type), β (A : Set v), (countable A β§β (f : v β u), SurjOn f A E)) :=
Goals accomplished!π
u: Type E: Set u
countable E ββ v A, countable A β§β f, SurjOn f A E
u: Type E: Set u
mp
countable E ββ v A, countable A β§β f, SurjOn f A E
u: Type E: Set u
(β v A, countable A β§β f, SurjOn f A E) β countable E
u: Type E: Set u
countable E ββ v A, countable A β§β f, SurjOn f A E
u: Type E: Set u
mp
countable E ββ v A, countable A β§β f, SurjOn f A E
u: Type E: Set u
mp
countable E ββ v A, countable A β§β f, SurjOn f A E
u: Type E: Set u
(β v A, countable A β§β f, SurjOn f A E) β countable E
u: Type E: Set u h_denomb: countable E
mp
β v A, countable A β§β f, SurjOn f A E
u: Type E: Set u
mp
countable E ββ v A, countable A β§β f, SurjOn f A E
u: Type E: Set u h_denomb: countable E
h
countable univ β§β f, SurjOn f univ E
u: Type E: Set u
mp
countable E ββ v A, countable A β§β f, SurjOn f A E
u: Type E: Set u h_denomb: countable E
h.left
countable univ
u: Type E: Set u h_denomb: countable E
β f, SurjOn f univ E
u: Type E: Set u
mp
countable E ββ v A, countable A β§β f, SurjOn f A E
u: Type E: Set u h_denomb: countable E
h.left
countable univ
u: Type E: Set u h_denomb: countable E
h.left
countable univ
u: Type E: Set u h_denomb: countable E
β f, SurjOn f univ E
Goals accomplished!π
u: Type E: Set u
mp
countable E ββ v A, countable A β§β f, SurjOn f A E
u: Type E: Set u f: β β u f_surj: SurjOn f univ E
h.right.intro
β f, SurjOn f univ E
u: Type E: Set u
mp
countable E ββ v A, countable A β§β f, SurjOn f A E
Goals accomplished!π
u: Type E: Set u
countable E ββ v A, countable A β§β f, SurjOn f A E
u: Type E: Set u h: β v A, countable A β§β f, SurjOn f A E
mpr
countable E
u: Type E: Set u
countable E ββ v A, countable A β§β f, SurjOn f A E
u: Type E: Set u v: Type A: Set v g: β β v g_surj: SurjOn g univ A f: v β u f_surj: SurjOn f A E
mpr.intro.intro.intro.intro.intro
countable E
u: Type E: Set u
countable E ββ v A, countable A β§β f, SurjOn f A E
u: Type E: Set u v: Type A: Set v g: β β v g_surj: SurjOn g univ A f: v β u f_surj: SurjOn f A E
mpr.intro.intro.intro.intro.intro
countable E
Goals accomplished!π
u: Type E: Set u v: Type A: Set v g: β β v g_surj: SurjOn g univ A f: v β u f_surj: SurjOn f A E
SurjOn (f β g) univ E
u: Type E: Set u v: Type A: Set v g: β β v g_surj: SurjOn g univ A f: v β u f_surj: SurjOn f A E
SurjOn (f β g) univ E
u: Type E: Set u v: Type A: Set v g: β β v g_surj: SurjOn g univ A f: v β u f_surj: SurjOn f A E
SurjOn (f β g) univ E
u: Type E: Set u v: Type A: Set v g: β β v g_surj: SurjOn g univ A f: v β u f_surj: SurjOn f A E e: u e_in_E: e β E
e β f β g '' univ
u: Type E: Set u v: Type A: Set v g: β β v g_surj: SurjOn g univ A f: v β u f_surj: SurjOn f A E
SurjOn (f β g) univ E
u: Type E: Set u v: Type A: Set v g: β β v g_surj: SurjOn g univ A f: v β u e: u e_in_E: e β E f_surj: e β f '' A
e β f β g '' univ
u: Type E: Set u v: Type A: Set v g: β β v g_surj: SurjOn g univ A f: v β u f_surj: SurjOn f A E
SurjOn (f β g) univ E
u: Type E: Set u v: Type A: Set v g: β β v g_surj: SurjOn g univ A f: v β u e: u e_in_E: e β E a: v a_in_A: a β A fa: f a = e
intro.intro
e β f β g '' univ
u: Type E: Set u v: Type A: Set v g: β β v g_surj: SurjOn g univ A f: v β u f_surj: SurjOn f A E
SurjOn (f β g) univ E
u: Type E: Set u v: Type A: Set v g: β β v f: v β u e: u e_in_E: e β E a: v a_in_A: a β A fa: f a = e g_surj: a β g '' univ
intro.intro
e β f β g '' univ
u: Type E: Set u v: Type A: Set v g: β β v g_surj: SurjOn g univ A f: v β u f_surj: SurjOn f A E
SurjOn (f β g) univ E
u: Type E: Set u v: Type A: Set v g: β β v f: v β u e: u e_in_E: e β E a: v a_in_A: a β A fa: f a = e n: β n_in_N: n β univ gn: g n = a
intro.intro.intro.intro
e β f β g '' univ
u: Type E: Set u v: Type A: Set v g: β β v g_surj: SurjOn g univ A f: v β u f_surj: SurjOn f A E
SurjOn (f β g) univ E
u: Type E: Set u v: Type A: Set v g: β β v f: v β u e: u e_in_E: e β E a: v a_in_A: a β A fa: f a = e n: β n_in_N: n β univ gn: g n = a
h
n β univ β§ (f β g) n = e
u: Type E: Set u v: Type A: Set v g: β β v g_surj: SurjOn g univ A f: v β u f_surj: SurjOn f A E
SurjOn (f β g) univ E
u: Type E: Set u v: Type A: Set v g: β β v f: v β u e: u e_in_E: e β E a: v a_in_A: a β A fa: f a = e n: β n_in_N: n β univ gn: g n = a
h.left
n β univ
u: Type E: Set u v: Type A: Set v g: β β v f: v β u e: u e_in_E: e β E a: v a_in_A: a β A fa: f a = e n: β n_in_N: n β univ gn: g n = a
(f β g) n = e
u: Type E: Set u v: Type A: Set v g: β β v g_surj: SurjOn g univ A f: v β u f_surj: SurjOn f A E
SurjOn (f β g) univ E
u: Type E: Set u v: Type A: Set v g: β β v f: v β u e: u e_in_E: e β E a: v a_in_A: a β A fa: f a = e n: β n_in_N: n β univ gn: g n = a
h.left
n β univ
u: Type E: Set u v: Type A: Set v g: β β v f: v β u e: u e_in_E: e β E a: v a_in_A: a β A fa: f a = e n: β n_in_N: n β univ gn: g n = a
h.left
n β univ
u: Type E: Set u v: Type A: Set v g: β β v f: v β u e: u e_in_E: e β E a: v a_in_A: a β A fa: f a = e n: β n_in_N: n β univ gn: g n = a
(f β g) n = e
Goals accomplished!π
u: Type E: Set u v: Type A: Set v g: β β v g_surj: SurjOn g univ A f: v β u f_surj: SurjOn f A E
SurjOn (f β g) univ E
u: Type E: Set u v: Type A: Set v g: β β v f: v β u e: u e_in_E: e β E a: v a_in_A: a β A fa: f a = e n: β n_in_N: n β univ gn: g n = a
h.right
f (g n) = e
u: Type E: Set u v: Type A: Set v g: β β v g_surj: SurjOn g univ A f: v β u f_surj: SurjOn f A E
SurjOn (f β g) univ E
u: Type E: Set u v: Type A: Set v g: β β v f: v β u e: u e_in_E: e β E a: v a_in_A: a β A fa: f a = e n: β n_in_N: n β univ gn: g n = a
h.right
f (g n) = e
u: Type E: Set u v: Type A: Set v g: β β v f: v β u e: u e_in_E: e β E a: v a_in_A: a β A fa: f a = e n: β n_in_N: n β univ gn: g n = a
h.right
f a = e
u: Type E: Set u v: Type A: Set v g: β β v f: v β u e: u e_in_E: e β E a: v a_in_A: a β A fa: f a = e n: β n_in_N: n β univ gn: g n = a
h.right
f a = e
Goals accomplished!π
u: Type E: Set u
countable E ββ v A, countable A β§β f, SurjOn f A E
Goals accomplished!π
/--Let E be a countable set. Then any A β E is countable.-/lemma subset_of_countable_set {u : Type} {E : Set u} (A : Set u) (h : A β E) (he : countable E) : countable A :=
Goals accomplished!π
u: Type E, A: Set u h: A β E he: countable E
countable A
u: Type E, A: Set u h: A β E he: countable E f:= fun e => e: u β u
countable A
u: Type E, A: Set u h: A β E he: countable E
countable A
u: Type E, A: Set u h: A β E he: countable E f:= fun e => e: u β u
countable A
Goals accomplished!π
u: Type E, A: Set u h: A β E he: countable E f:= fun e => e: u β u
SurjOn f E A
u: Type E, A: Set u h: A β E he: countable E f:= fun e => e: u β u
SurjOn f E A
u: Type E, A: Set u h: A β E he: countable E f:= fun e => e: u β u
SurjOn f E A
u: Type E, A: Set u h: A β E he: countable E f:= fun e => e: u β u a: u a_in_A: a β A
a β f '' E
u: Type E, A: Set u h: A β E he: countable E f:= fun e => e: u β u
SurjOn f E A
Goals accomplished!π
Goals accomplished!π
u: Type E, A: Set u h: A β E he: countable E
countable A
Goals accomplished!π
theorem prod_pow_primes_left {p q : β} [hp : Fact p.Prime] [hq : Fact q.Prime]
(n m : β) (neq : p β q) : padicValNat p (p^n * q^m) = n :=
Goals accomplished!π
p, q: β hp: Fact (Nat.Prime p) hq: Fact (Nat.Prime q) n, m: β neq: p β q
padicValNat p (p ^ n * q ^ m) = n
p, q: β hp: Fact (Nat.Prime p) hq: Fact (Nat.Prime q) n, m: β neq: p β q
padicValNat p (p ^ n * q ^ m) = n
p, q: β hp: Fact (Nat.Prime p) hq: Fact (Nat.Prime q) n, m: β neq: p β q
padicValNat p (p ^ n) + padicValNat p (q ^ m) = n
p, q: β hp: Fact (Nat.Prime p) hq: Fact (Nat.Prime q) n, m: β neq: p β q
padicValNat p (p ^ n) + padicValNat p (q ^ m) = n
p, q: β hp: Fact (Nat.Prime p) hq: Fact (Nat.Prime q) n, m: β neq: p β q
padicValNat p (p ^ n * q ^ m) = n
p, q: β hp: Fact (Nat.Prime p) hq: Fact (Nat.Prime q) n, m: β neq: p β q
padicValNat p (p ^ n) + padicValNat p (q ^ m) = n
Goals accomplished!π
p, q: β hp: Fact (Nat.Prime p) hq: Fact (Nat.Prime q) n, m: β neq: p β q
padicValNat p (p ^ n) + padicValNat p (q ^ m) = n
p, q: β hp: Fact (Nat.Prime p) hq: Fact (Nat.Prime q) n, m: β neq: p β q
padicValNat p (q ^ m) =0
p, q: β hp: Fact (Nat.Prime p) hq: Fact (Nat.Prime q) n, m: β neq: p β q
m * padicValNat p q =0
p, q: β hp: Fact (Nat.Prime p) hq: Fact (Nat.Prime q) n, m: β neq: p β q
padicValNat p (q ^ m) =0
p, q: β hp: Fact (Nat.Prime p) hq: Fact (Nat.Prime q) n, m: β neq: p β q
m *0=0
p, q: β hp: Fact (Nat.Prime p) hq: Fact (Nat.Prime q) n, m: β neq: p β q
padicValNat p (q ^ m) =0
p, q: β hp: Fact (Nat.Prime p) hq: Fact (Nat.Prime q) n, m: β neq: p β q
0=0
Goals accomplished!π
p, q: β hp: Fact (Nat.Prime p) hq: Fact (Nat.Prime q) n, m: β neq: p β q
padicValNat p (p ^ n * q ^ m) = n
p, q: β hp: Fact (Nat.Prime p) hq: Fact (Nat.Prime q) n, m: β neq: p β q padic_p_qm_eq_0: padicValNat p (q ^ m) =0
padicValNat p (p ^ n) + padicValNat p (q ^ m) = n
p, q: β hp: Fact (Nat.Prime p) hq: Fact (Nat.Prime q) n, m: β neq: p β q padic_p_qm_eq_0: padicValNat p (q ^ m) =0
n + padicValNat p (q ^ m) = n
p, q: β hp: Fact (Nat.Prime p) hq: Fact (Nat.Prime q) n, m: β neq: p β q padic_p_qm_eq_0: padicValNat p (q ^ m) =0
padicValNat p (p ^ n) + padicValNat p (q ^ m) = n
p, q: β hp: Fact (Nat.Prime p) hq: Fact (Nat.Prime q) n, m: β neq: p β q padic_p_qm_eq_0: padicValNat p (q ^ m) =0
n +0= n
p, q: β hp: Fact (Nat.Prime p) hq: Fact (Nat.Prime q) n, m: β neq: p β q padic_p_qm_eq_0: padicValNat p (q ^ m) =0
padicValNat p (p ^ n) + padicValNat p (q ^ m) = n
p, q: β hp: Fact (Nat.Prime p) hq: Fact (Nat.Prime q) n, m: β neq: p β q padic_p_qm_eq_0: padicValNat p (q ^ m) =0
/--βΒ² is countable.-/lemma N2_countable : countable (univ : Set (β Γ β)) :=
Goals accomplished!π
countable univ
A:= {n |β a b, n =2^ a *3^ b}: Set β
countable univ
countable univ
A:= {n |β a b, n =2^ a *3^ b}: Set β f:= fun n =>if n β A then (n.factorization 2, n.factorization 3) else (0, 0): β β β Γ β
countable univ
countable univ
A:= {n |β a b, n =2^ a *3^ b}: Set β f:= fun n =>if n β A then (n.factorization 2, n.factorization 3) else (0, 0): β β β Γ β
countable univ
Goals accomplished!π
A:= {n |β a b, n =2^ a *3^ b}: Set β f:= fun n =>if n β A then (n.factorization 2, n.factorization 3) else (0, 0): β β β Γ β
SurjOn f A univ
A:= {n |β a b, n =2^ a *3^ b}: Set β f:= fun n =>if n β A then (n.factorization 2, n.factorization 3) else (0, 0): β β β Γ β
SurjOn f A univ
A:= {n |β a b, n =2^ a *3^ b}: Set β f:= fun n =>if n β A then (n.factorization 2, n.factorization 3) else (0, 0): β β β Γ β
SurjOn f A univ
A:= {n |β a b, n =2^ a *3^ b}: Set β f:= fun n =>if n β A then (n.factorization 2, n.factorization 3) else (0, 0): β β β Γ β x: β Γ β aβ: x β univ
x β f '' A
A:= {n |β a b, n =2^ a *3^ b}: Set β f:= fun n =>if n β A then (n.factorization 2, n.factorization 3) else (0, 0): β β β Γ β
SurjOn f A univ
A:= {n |β a b, n =2^ a *3^ b}: Set β f:= fun n =>if n β A then (n.factorization 2, n.factorization 3) else (0, 0): β β β Γ β x: β Γ β aβ: x β univ n:= 2^ x.1 *3^ x.2: β
x β f '' A
A:= {n |β a b, n =2^ a *3^ b}: Set β f:= fun n =>if n β A then (n.factorization 2, n.factorization 3) else (0, 0): β β β Γ β
SurjOn f A univ
A:= {n |β a b, n =2^ a *3^ b}: Set β f:= fun n =>if n β A then (n.factorization 2, n.factorization 3) else (0, 0): β β β Γ β x: β Γ β aβ: x β univ n:= 2^ x.1 *3^ x.2: β
h
n β A β§ f n = x
A:= {n |β a b, n =2^ a *3^ b}: Set β f:= fun n =>if n β A then (n.factorization 2, n.factorization 3) else (0, 0): β β β Γ β
SurjOn f A univ
A:= {n |β a b, n =2^ a *3^ b}: Set β f:= fun n =>if n β A then (n.factorization 2, n.factorization 3) else (0, 0): β β β Γ β x: β Γ β aβ: x β univ n:= 2^ x.1 *3^ x.2: β n_in_A: n β A
h
n β A β§ f n = x
A:= {n |β a b, n =2^ a *3^ b}: Set β f:= fun n =>if n β A then (n.factorization 2, n.factorization 3) else (0, 0): β β β Γ β
SurjOn f A univ
A:= {n |β a b, n =2^ a *3^ b}: Set β f:= fun n =>if n β A then (n.factorization 2, n.factorization 3) else (0, 0): β β β Γ β x: β Γ β aβ: x β univ n:= 2^ x.1 *3^ x.2: β n_in_A: n β A
h
f n = x
A:= {n |β a b, n =2^ a *3^ b}: Set β f:= fun n =>if n β A then (n.factorization 2, n.factorization 3) else (0, 0): β β β Γ β
SurjOn f A univ
A:= {n |β a b, n =2^ a *3^ b}: Set β f:= fun n =>if n β A then (n.factorization 2, n.factorization 3) else (0, 0): β β β Γ β x: β Γ β aβ: x β univ n:= 2^ x.1 *3^ x.2: β n_in_A: n β A
h
f n = x
A:= {n |β a b, n =2^ a *3^ b}: Set β f:= fun n =>if n β A then (n.factorization 2, n.factorization 3) else (0, 0): β β β Γ β x: β Γ β aβ: x β univ n:= 2^ x.1 *3^ x.2: β n_in_A: n β A
h
f n = x
Goals accomplished!π
A:= {n |β a b, n =2^ a *3^ b}: Set β f:= fun n =>if n β A then (n.factorization 2, n.factorization 3) else (0, 0): β β β Γ β x: β Γ β aβ: x β univ n:= 2^ x.1 *3^ x.2: β n_in_A: n β A
h
(if n β A then (n.factorization 2, n.factorization 3) else (0, 0)) = x
A:= {n |β a b, n =2^ a *3^ b}: Set β f:= fun n =>if n β A then (n.factorization 2, n.factorization 3) else (0, 0): β β β Γ β
SurjOn f A univ
[Meta.Tactic.simp.rewrite] if_pos:1000, if n β A then (n.factorization 2, n.factorization 3)
else (0, 0) ==> (n.factorization 2, n.factorization 3)
[Meta.Tactic.simp.rewrite] if_pos:1000, if n β A then (n.factorization 2, n.factorization 3)
else (0, 0) ==> (n.factorization 2, n.factorization 3)
A:= {n |β a b, n =2^ a *3^ b}: Set β f:= fun n =>if n β A then (n.factorization 2, n.factorization 3) else (0, 0): β β β Γ β x: β Γ β aβ: x β univ n:= 2^ x.1 *3^ x.2: β n_in_A, hβ: n β A
h.isTrue
(n.factorization 2, n.factorization 3) = x
A:= {n |β a b, n =2^ a *3^ b}: Set β f:= fun n =>if n β A then (n.factorization 2, n.factorization 3) else (0, 0): β β β Γ β x: β Γ β aβ: x β univ n:= 2^ x.1 *3^ x.2: β n_in_A: n β A hβ: n β A
(n.factorization 2, n.factorization 3) = x
A:= {n |β a b, n =2^ a *3^ b}: Set β f:= fun n =>if n β A then (n.factorization 2, n.factorization 3) else (0, 0): β β β Γ β
SurjOn f A univ
A:= {n |β a b, n =2^ a *3^ b}: Set β f:= fun n =>if n β A then (n.factorization 2, n.factorization 3) else (0, 0): β β β Γ β x: β Γ β aβ: x β univ n:= 2^ x.1 *3^ x.2: β n_in_A, hβ: n β A
h.isTrue
(n.factorization 2, n.factorization 3) = x
A:= {n |β a b, n =2^ a *3^ b}: Set β f:= fun n =>if n β A then (n.factorization 2, n.factorization 3) else (0, 0): β β β Γ β x: β Γ β aβ: x β univ n:= 2^ x.1 *3^ x.2: β n_in_A, hβ: n β A
h.isTrue
(n.factorization 2, n.factorization 3) = x
A:= {n |β a b, n =2^ a *3^ b}: Set β f:= fun n =>if n β A then (n.factorization 2, n.factorization 3) else (0, 0): β β β Γ β x: β Γ β aβ: x β univ n:= 2^ x.1 *3^ x.2: β n_in_A: n β A hβ: n β A
(n.factorization 2, n.factorization 3) = x
A:= {n |β a b, n =2^ a *3^ b}: Set β f:= fun n =>if n β A then (n.factorization 2, n.factorization 3) else (0, 0): β β β Γ β x: β Γ β aβ: x β univ n:= 2^ x.1 *3^ x.2: β n_in_A, hβ: n β A
h.isTrue
(n.factorization 2, n.factorization 3) = x
A:= {n |β a b, n =2^ a *3^ b}: Set β f:= fun n =>if n β A then (n.factorization 2, n.factorization 3) else (0, 0): β β β Γ β x: β Γ β aβ: x β univ n:= 2^ x.1 *3^ x.2: β n_in_A, hβ: n β A
h.isTrue
(n.factorization 2, n.factorization 3) = x
Goals accomplished!π
A:= {n |β a b, n =2^ a *3^ b}: Set β f:= fun n =>if n β A then (n.factorization 2, n.factorization 3) else (0, 0): β β β Γ β x: β Γ β aβ: x β univ n:= 2^ x.1 *3^ x.2: β n_in_A, hβ: n β A
h.isTrue
(padicValNat 2 n, n.factorization 3) = x
A:= {n |β a b, n =2^ a *3^ b}: Set β f:= fun n =>if n β A then (n.factorization 2, n.factorization 3) else (0, 0): β β β Γ β x: β Γ β aβ: x β univ n:= 2^ x.1 *3^ x.2: β n_in_A, hβ: n β A
h.isTrue
(n.factorization 2, n.factorization 3) = x
A:= {n |β a b, n =2^ a *3^ b}: Set β f:= fun n =>if n β A then (n.factorization 2, n.factorization 3) else (0, 0): β β β Γ β x: β Γ β aβ: x β univ n:= 2^ x.1 *3^ x.2: β n_in_A, hβ: n β A
h.isTrue
(padicValNat 2 n, n.factorization 3) = x
Goals accomplished!π
A:= {n |β a b, n =2^ a *3^ b}: Set β f:= fun n =>if n β A then (n.factorization 2, n.factorization 3) else (0, 0): β β β Γ β x: β Γ β aβ: x β univ n:= 2^ x.1 *3^ x.2: β n_in_A, hβ: n β A
h.isTrue
(padicValNat 2 n, padicValNat 3 n) = x
A:= {n |β a b, n =2^ a *3^ b}: Set β f:= fun n =>if n β A then (n.factorization 2, n.factorization 3) else (0, 0): β β β Γ β x: β Γ β aβ: x β univ n:= 2^ x.1 *3^ x.2: β n_in_A, hβ: n β A
h.isTrue
(n.factorization 2, n.factorization 3) = x
A:= {n |β a b, n =2^ a *3^ b}: Set β f:= fun n =>if n β A then (n.factorization 2, n.factorization 3) else (0, 0): β β β Γ β x: β Γ β aβ: x β univ n:= 2^ x.1 *3^ x.2: β n_in_A, hβ: n β A
h.isTrue
(padicValNat 2 n, padicValNat 3 n) = x
A:= {n |β a b, n =2^ a *3^ b}: Set β f:= fun n =>if n β A then (n.factorization 2, n.factorization 3) else (0, 0): β β β Γ β x: β Γ β aβ: x β univ n:= 2^ x.1 *3^ x.2: β n_in_A, hβ: n β A
A:= {n |β a b, n =2^ a *3^ b}: Set β f:= fun n =>if n β A then (n.factorization 2, n.factorization 3) else (0, 0): β β β Γ β x: β Γ β aβ: x β univ n:= 2^ x.1 *3^ x.2: β n_in_A, hβ: n β A
h.isTrue
(x.1, padicValNat 3 n) = x
A:= {n |β a b, n =2^ a *3^ b}: Set β f:= fun n =>if n β A then (n.factorization 2, n.factorization 3) else (0, 0): β β β Γ β x: β Γ β aβ: x β univ n:= 2^ x.1 *3^ x.2: β n_in_A, hβ: n β A
h.isTrue
(padicValNat 2 n, padicValNat 3 n) = x
A:= {n |β a b, n =2^ a *3^ b}: Set β f:= fun n =>if n β A then (n.factorization 2, n.factorization 3) else (0, 0): β β β Γ β x: β Γ β aβ: x β univ n:= 2^ x.1 *3^ x.2: β n_in_A, hβ: n β A
A:= {n |β a b, n =2^ a *3^ b}: Set β f:= fun n =>if n β A then (n.factorization 2, n.factorization 3) else (0, 0): β β β Γ β x: β Γ β aβ: x β univ n:= 2^ x.1 *3^ x.2: β n_in_A, hβ: n β A
h.isTrue
(x.1, x.2) = x
Goals accomplished!π
A:= {n |β a b, n =2^ a *3^ b}: Set β f:= fun n =>if n β A then (n.factorization 2, n.factorization 3) else (0, 0): β β β Γ β
SurjOn f A univ
Goals accomplished!π
Goals accomplished!π
countable univ
Goals accomplished!π
/--We use a definition of a set being countable different to Mathlib's to match the book as much as possible. For completeness, we show that our definition is equivalent to Mathlib's. It corresponds to Corollary 1.5.-/lemma countable_iff {u : Type} {E : Set u} (hE : Set.Nonempty E) : countable E β Set.Countable E :=
Goals accomplished!π
u: Type E: Set u hE: E.Nonempty
countable E β E.Countable
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type
countable E β E.Countable
u: Type E: Set u hE: E.Nonempty
countable E β E.Countable
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type
mp
countable E β E.Countable
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type
E.Countable β countable E
u: Type E: Set u hE: E.Nonempty
countable E β E.Countable
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type
mp
countable E β E.Countable
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type
mp
countable E β E.Countable
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type
E.Countable β countable E
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type h: countable E
mp
E.Countable
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type
mp
countable E β E.Countable
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: β β u f_surj: SurjOn f univ E
mp.intro
E.Countable
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type
mp
countable E β E.Countable
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: β β u f_surj: SurjOn f univ E
mp.intro
E.Countable
Goals accomplished!π
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: β β u f_surj: SurjOn f univ E
β e β E, β n, f n = e
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: β β u f_surj: SurjOn f univ E
β e β E, β n, f n = e
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: β β u f_surj: SurjOn f univ E
β e β E, β n, f n = e
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: β β u f_surj: SurjOn f univ E e: u e_in_E: e β E
β n, f n = e
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: β β u f_surj: SurjOn f univ E
β e β E, β n, f n = e
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: β β u e: u e_in_E: e β E f_surj: e β f '' univ
β n, f n = e
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: β β u f_surj: SurjOn f univ E
β e β E, β n, f n = e
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: β β u e: u e_in_E: e β E n: β leftβ: n β univ f_n: f n = e
intro.intro
β n, f n = e
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: β β u f_surj: SurjOn f univ E
β e β E, β n, f n = e
Goals accomplished!π
Goals accomplished!π
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type
mp
countable E β E.Countable
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: β β u f_surj: SurjOn f univ E surj': β e β E, β n, f n = e g:= fun e => Nat.find β―: s_t β β
mp.intro
E.Countable
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type
mp
countable E β E.Countable
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: β β u f_surj: SurjOn f univ E surj': β e β E, β n, f n = e g:= fun e => Nat.find β―: s_t β β
mp.intro
E.Countable
Goals accomplished!π
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: β β u f_surj: SurjOn f univ E surj': β e β E, β n, f n = e g:= fun e => Nat.find β―: s_t β β
Function.Injective g
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: β β u f_surj: SurjOn f univ E surj': β e β E, β n, f n = e g:= fun e => Nat.find β―: s_t β β
Function.Injective g
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: β β u f_surj: SurjOn f univ E surj': β e β E, β n, f n = e g:= fun e => Nat.find β―: s_t β β
Function.Injective g
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: β β u f_surj: SurjOn f univ E surj': β e β E, β n, f n = e g:= fun e => Nat.find β―: s_t β β
Function.Injective g
Goals accomplished!π
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: β β u f_surj: SurjOn f univ E surj': β e β E, β n, f n = e g:= fun e => Nat.find β―: s_t β β
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: β β u f_surj: SurjOn f univ E surj': β e β E, β n, f n = e g:= fun e => Nat.find β―: s_t β β
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: β β u f_surj: SurjOn f univ E surj': β e β E, β n, f n = e g:= fun e => Nat.find β―: s_t β β
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: β β u f_surj: SurjOn f univ E surj': β e β E, β n, f n = e g:= fun e => Nat.find β―: s_t β β e: u he: e β E
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: β β u f_surj: SurjOn f univ E surj': β e β E, β n, f n = e g:= fun e => Nat.find β―: s_t β β
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: β β u f_surj: SurjOn f univ E surj': β e β E, β n, f n = e g:= fun e => Nat.find β―: s_t β β e: u he: e β E
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: β β u f_surj: SurjOn f univ E surj': β e β E, β n, f n = e g:= fun e => Nat.find β―: s_t β β e: u he: e β E
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: β β u f_surj: SurjOn f univ E surj': β e β E, β n, f n = e g:= fun e => Nat.find β―: s_t β β
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: β β u f_surj: SurjOn f univ E surj': β e β E, β n, f n = e g:= fun e => Nat.find β―: s_t β β
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: β β u f_surj: SurjOn f univ E surj': β e β E, β n, f n = e g:= fun e => Nat.find β―: s_t β β
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: β β u f_surj: SurjOn f univ E surj': β e β E, β n, f n = e g:= fun e => Nat.find β―: s_t β β
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: β β u f_surj: SurjOn f univ E surj': β e β E, β n, f n = e g:= fun e => Nat.find β―: s_t β β
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type
mp
countable E β E.Countable
Goals accomplished!π
u: Type E: Set u hE: E.Nonempty
countable E β E.Countable
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type h: E.Countable
mpr
countable E
u: Type E: Set u hE: E.Nonempty
countable E β E.Countable
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: βE β β f_inj: Function.Injective f
mpr.mk.intro
countable E
u: Type E: Set u hE: E.Nonempty
countable E β E.Countable
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: βE β β f_inj: Function.Injective f fE:= {n |β e, f e = n}: Set β
mpr.mk.intro
countable E
u: Type E: Set u hE: E.Nonempty
countable E β E.Countable
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: βE β β f_inj: Function.Injective f fE:= {n |β e, f e = n}: Set β fE_countable: countable fE
mpr.mk.intro
countable E
u: Type E: Set u hE: E.Nonempty
countable E β E.Countable
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: βE β β f_inj: Function.Injective f fE:= {n |β e, f e = n}: Set β fE_countable: countable fE
mpr.mk.intro
countable E
Goals accomplished!π
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: βE β β f_inj: Function.Injective f fE:= {n |β e, f e = n}: Set β fE_countable: countable fE
β n β fE, {e | f e = n}.Nonempty
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: βE β β f_inj: Function.Injective f fE:= {n |β e, f e = n}: Set β fE_countable: countable fE
β n β fE, {e | f e = n}.Nonempty
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: βE β β f_inj: Function.Injective f fE:= {n |β e, f e = n}: Set β fE_countable: countable fE
β n β fE, {e | f e = n}.Nonempty
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: βE β β f_inj: Function.Injective f fE:= {n |β e, f e = n}: Set β fE_countable: countable fE n: β hn: n β fE
{e | f e = n}.Nonempty
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: βE β β f_inj: Function.Injective f fE:= {n |β e, f e = n}: Set β fE_countable: countable fE
β n β fE, {e | f e = n}.Nonempty
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: βE β β f_inj: Function.Injective f fE:= {n |β e, f e = n}: Set β fE_countable: countable fE n: β e: s_t fe_n: f e = n
intro
{e | f e = n}.Nonempty
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: βE β β f_inj: Function.Injective f fE:= {n |β e, f e = n}: Set β fE_countable: countable fE
β n β fE, {e | f e = n}.Nonempty
Goals accomplished!π
Goals accomplished!π
u: Type E: Set u hE: E.Nonempty
countable E β E.Countable
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: βE β β f_inj: Function.Injective f fE:= {n |β e, f e = n}: Set β fE_countable: countable fE fE_dual_non_empty: β n β fE, {e | f e = n}.Nonempty Ο:= fun n h =>β―.some: (n : β) β n β fE ββE
mpr.mk.intro
countable E
u: Type E: Set u hE: E.Nonempty
countable E β E.Countable
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: βE β β f_inj: Function.Injective f fE:= {n |β e, f e = n}: Set β fE_countable: countable fE fE_dual_non_empty: β n β fE, {e | f e = n}.Nonempty Ο:= fun n h =>β―.some: (n : β) β n β fE ββE f':= fun n =>if h : n β fE thenβ(Ο n h) else hE.some: β β u
mpr.mk.intro
countable E
u: Type E: Set u hE: E.Nonempty
countable E β E.Countable
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: βE β β f_inj: Function.Injective f fE:= {n |β e, f e = n}: Set β fE_countable: countable fE fE_dual_non_empty: β n β fE, {e | f e = n}.Nonempty Ο:= fun n h =>β―.some: (n : β) β n β fE ββE f':= fun n =>if h : n β fE thenβ(Ο n h) else hE.some: β β u
mpr.mk.intro
countable E
Goals accomplished!π
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: βE β β f_inj: Function.Injective f fE:= {n |β e, f e = n}: Set β fE_countable: countable fE fE_dual_non_empty: β n β fE, {e | f e = n}.Nonempty Ο:= fun n h =>β―.some: (n : β) β n β fE ββE f':= fun n =>if h : n β fE thenβ(Ο n h) else hE.some: β β u
SurjOn f' fE E
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: βE β β f_inj: Function.Injective f fE:= {n |β e, f e = n}: Set β fE_countable: countable fE fE_dual_non_empty: β n β fE, {e | f e = n}.Nonempty Ο:= fun n h =>β―.some: (n : β) β n β fE ββE f':= fun n =>if h : n β fE thenβ(Ο n h) else hE.some: β β u
SurjOn f' fE E
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: βE β β f_inj: Function.Injective f fE:= {n |β e, f e = n}: Set β fE_countable: countable fE fE_dual_non_empty: β n β fE, {e | f e = n}.Nonempty Ο:= fun n h =>β―.some: (n : β) β n β fE ββE f':= fun n =>if h : n β fE thenβ(Ο n h) else hE.some: β β u
SurjOn f' fE E
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: βE β β f_inj: Function.Injective f fE:= {n |β e, f e = n}: Set β fE_countable: countable fE fE_dual_non_empty: β n β fE, {e | f e = n}.Nonempty Ο:= fun n h =>β―.some: (n : β) β n β fE ββE f':= fun n =>if h : n β fE thenβ(Ο n h) else hE.some: β β u e: u e_in_E: e β E
e β f' '' fE
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: βE β β f_inj: Function.Injective f fE:= {n |β e, f e = n}: Set β fE_countable: countable fE fE_dual_non_empty: β n β fE, {e | f e = n}.Nonempty Ο:= fun n h =>β―.some: (n : β) β n β fE ββE f':= fun n =>if h : n β fE thenβ(Ο n h) else hE.some: β β u
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: βE β β f_inj: Function.Injective f fE:= {n |β e, f e = n}: Set β fE_countable: countable fE fE_dual_non_empty: β n β fE, {e | f e = n}.Nonempty Ο:= fun n h =>β―.some: (n : β) β n β fE ββE f':= fun n =>if h : n β fE thenβ(Ο n h) else hE.some: β β u
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: βE β β f_inj: Function.Injective f fE:= {n |β e, f e = n}: Set β fE_countable: countable fE fE_dual_non_empty: β n β fE, {e | f e = n}.Nonempty Ο:= fun n h =>β―.some: (n : β) β n β fE ββE f':= fun n =>if h : n β fE thenβ(Ο n h) else hE.some: β β u
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: βE β β f_inj: Function.Injective f fE:= {n |β e, f e = n}: Set β fE_countable: countable fE fE_dual_non_empty: β n β fE, {e | f e = n}.Nonempty Ο:= fun n h =>β―.some: (n : β) β n β fE ββE f':= fun n =>if h : n β fE thenβ(Ο n h) else hE.some: β β u
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: βE β β f_inj: Function.Injective f fE:= {n |β e, f e = n}: Set β fE_countable: countable fE fE_dual_non_empty: β n β fE, {e | f e = n}.Nonempty Ο:= fun n h =>β―.some: (n : β) β n β fE ββE f':= fun n =>if h : n β fE thenβ(Ο n h) else hE.some: β β u
(if h : f e' β fE thenβ(Ο (f e') h) else hE.some) = e
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: βE β β f_inj: Function.Injective f fE:= {n |β e, f e = n}: Set β fE_countable: countable fE fE_dual_non_empty: β n β fE, {e | f e = n}.Nonempty Ο:= fun n h =>β―.some: (n : β) β n β fE ββE f':= fun n =>if h : n β fE thenβ(Ο n h) else hE.some: β β u
SurjOn f' fE E
[Meta.Tactic.simp.rewrite] dif_pos:1000, if h : f e' β fE thenβ(Ο (f e') h) else hE.some ==>β(Ο (f e') hβ)
[Meta.Tactic.simp.rewrite] dif_pos:1000, if h : f e' β fE thenβ(Ο (f e') h) else hE.some ==>β(Ο (f e') fe'_in_fE)
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: βE β β f_inj: Function.Injective f fE:= {n |β e, f e = n}: Set β fE_countable: countable fE fE_dual_non_empty: β n β fE, {e | f e = n}.Nonempty Ο:= fun n h =>β―.some: (n : β) β n β fE ββE f':= fun n =>if h : n β fE thenβ(Ο n h) else hE.some: β β u
u: Type E: Set u hE: E.Nonempty s_t:= { e // e β E }: Type f: βE β β f_inj: Function.Injective f fE:= {n |β e, f e = n}: Set β fE_countable: countable fE fE_dual_non_empty: β n β fE, {e | f e = n}.Nonempty Ο:= fun n h =>β―.some: (n : β) β n β fE ββE f':= fun n =>if h : n β fE thenβ(Ο n h) else hE.some: β β u
SurjOn f' fE E
Goals accomplished!π
Goals accomplished!π
u: Type E: Set u hE: E.Nonempty
countable E β E.Countable
Goals accomplished!π
/--The product of two countable sets is countable. (Proposition 1.6 p.2)-/lemma product_countable_set {u v : Type} {E : Set u} {A : Set v} (he : countable E) (ha : countable A) : countable {x : u Γ v | x.1 β E β§ x.2 β A} :=
Goals accomplished!π
u, v: Type E: Set u A: Set v he: countable E ha: countable A
countable {x | x.1 β E β§ x.2 β A}
u, v: Type E: Set u A: Set v ha: countable A fe: β β u fe_surj: SurjOn fe univ E
intro
countable {x | x.1 β E β§ x.2 β A}
u, v: Type E: Set u A: Set v he: countable E ha: countable A
countable {x | x.1 β E β§ x.2 β A}
u, v: Type E: Set u A: Set v fe: β β u fe_surj: SurjOn fe univ E fa: β β v fa_surj: SurjOn fa univ A
intro.intro
countable {x | x.1 β E β§ x.2 β A}
u, v: Type E: Set u A: Set v he: countable E ha: countable A
countable {x | x.1 β E β§ x.2 β A}
u, v: Type E: Set u A: Set v fe: β β u fe_surj: SurjOn fe univ E fa: β β v fa_surj: SurjOn fa univ A Ο:= fun x => (fe x.1, fa x.2): β Γ β β u Γ v
intro.intro
countable {x | x.1 β E β§ x.2 β A}
u, v: Type E: Set u A: Set v he: countable E ha: countable A
countable {x | x.1 β E β§ x.2 β A}
u, v: Type E: Set u A: Set v fe: β β u fe_surj: SurjOn fe univ E fa: β β v fa_surj: SurjOn fa univ A Ο:= fun x => (fe x.1, fa x.2): β Γ β β u Γ v
intro.intro
countable {x | x.1 β E β§ x.2 β A}
Goals accomplished!π
u, v: Type E: Set u A: Set v fe: β β u fe_surj: SurjOn fe univ E fa: β β v fa_surj: SurjOn fa univ A Ο:= fun x => (fe x.1, fa x.2): β Γ β β u Γ v
SurjOn Ο univ {x | x.1 β E β§ x.2 β A}
u, v: Type E: Set u A: Set v fe: β β u fe_surj: SurjOn fe univ E fa: β β v fa_surj: SurjOn fa univ A Ο:= fun x => (fe x.1, fa x.2): β Γ β β u Γ v
SurjOn Ο univ {x | x.1 β E β§ x.2 β A}
u, v: Type E: Set u A: Set v fe: β β u fe_surj: SurjOn fe univ E fa: β β v fa_surj: SurjOn fa univ A Ο:= fun x => (fe x.1, fa x.2): β Γ β β u Γ v
SurjOn Ο univ {x | x.1 β E β§ x.2 β A}
u, v: Type E: Set u A: Set v fe: β β u fe_surj: SurjOn fe univ E fa: β β v fa_surj: SurjOn fa univ A Ο:= fun x => (fe x.1, fa x.2): β Γ β β u Γ v x: u Γ v hx1: x.1 β E hx2: x.2 β A
x β Ο '' univ
u, v: Type E: Set u A: Set v fe: β β u fe_surj: SurjOn fe univ E fa: β β v fa_surj: SurjOn fa univ A Ο:= fun x => (fe x.1, fa x.2): β Γ β β u Γ v
SurjOn Ο univ {x | x.1 β E β§ x.2 β A}
u, v: Type E: Set u A: Set v fe: β β u fe_surj: SurjOn fe univ E fa: β β v fa_surj: SurjOn fa univ A Ο:= fun x => (fe x.1, fa x.2): β Γ β β u Γ v x: u Γ v hx1: x.1 β E hx2: x.2 β A e: β leftβ: e β univ hfe: fe e = x.1
intro.intro
x β Ο '' univ
u, v: Type E: Set u A: Set v fe: β β u fe_surj: SurjOn fe univ E fa: β β v fa_surj: SurjOn fa univ A Ο:= fun x => (fe x.1, fa x.2): β Γ β β u Γ v
SurjOn Ο univ {x | x.1 β E β§ x.2 β A}
u, v: Type E: Set u A: Set v fe: β β u fe_surj: SurjOn fe univ E fa: β β v fa_surj: SurjOn fa univ A Ο:= fun x => (fe x.1, fa x.2): β Γ β β u Γ v x: u Γ v hx1: x.1 β E hx2: x.2 β A e: β leftβΒΉ: e β univ hfe: fe e = x.1 a: β leftβ: a β univ hfa: fa a = x.2
intro.intro.intro.intro
x β Ο '' univ
u, v: Type E: Set u A: Set v fe: β β u fe_surj: SurjOn fe univ E fa: β β v fa_surj: SurjOn fa univ A Ο:= fun x => (fe x.1, fa x.2): β Γ β β u Γ v
SurjOn Ο univ {x | x.1 β E β§ x.2 β A}
u, v: Type E: Set u A: Set v fe: β β u fe_surj: SurjOn fe univ E fa: β β v fa_surj: SurjOn fa univ A Ο:= fun x => (fe x.1, fa x.2): β Γ β β u Γ v x: u Γ v hx1: x.1 β E hx2: x.2 β A e: β leftβΒΉ: e β univ hfe: fe e = x.1 a: β leftβ: a β univ hfa: fa a = x.2
h
(e, a) β univ β§ Ο (e, a) = x
u, v: Type E: Set u A: Set v fe: β β u fe_surj: SurjOn fe univ E fa: β β v fa_surj: SurjOn fa univ A Ο:= fun x => (fe x.1, fa x.2): β Γ β β u Γ v
SurjOn Ο univ {x | x.1 β E β§ x.2 β A}
u, v: Type E: Set u A: Set v fe: β β u fe_surj: SurjOn fe univ E fa: β β v fa_surj: SurjOn fa univ A Ο:= fun x => (fe x.1, fa x.2): β Γ β β u Γ v x: u Γ v hx1: x.1 β E hx2: x.2 β A e: β leftβΒΉ: e β univ hfe: fe e = x.1 a: β leftβ: a β univ hfa: fa a = x.2
h
Ο (e, a) = x
u, v: Type E: Set u A: Set v fe: β β u fe_surj: SurjOn fe univ E fa: β β v fa_surj: SurjOn fa univ A Ο:= fun x => (fe x.1, fa x.2): β Γ β β u Γ v
SurjOn Ο univ {x | x.1 β E β§ x.2 β A}
u, v: Type E: Set u A: Set v fe: β β u fe_surj: SurjOn fe univ E fa: β β v fa_surj: SurjOn fa univ A Ο:= fun x => (fe x.1, fa x.2): β Γ β β u Γ v x: u Γ v hx1: x.1 β E hx2: x.2 β A e: β leftβΒΉ: e β univ hfe: fe e = x.1 a: β leftβ: a β univ hfa: fa a = x.2
h
Ο (e, a) = x
u, v: Type E: Set u A: Set v fe: β β u fe_surj: SurjOn fe univ E fa: β β v fa_surj: SurjOn fa univ A Ο:= fun x => (fe x.1, fa x.2): β Γ β β u Γ v x: u Γ v hx1: x.1 β E hx2: x.2 β A e: β leftβΒΉ: e β univ hfe: fe e = x.1 a: β leftβ: a β univ hfa: fa a = x.2
h
Ο (e, a) = x
Goals accomplished!π
u, v: Type E: Set u A: Set v fe: β β u fe_surj: SurjOn fe univ E fa: β β v fa_surj: SurjOn fa univ A Ο:= fun x => (fe x.1, fa x.2): β Γ β β u Γ v x: u Γ v hx1: x.1 β E hx2: x.2 β A e: β leftβΒΉ: e β univ hfe: fe e = x.1 a: β leftβ: a β univ hfa: fa a = x.2
h
(fe e, fa a) = x
u, v: Type E: Set u A: Set v fe: β β u fe_surj: SurjOn fe univ E fa: β β v fa_surj: SurjOn fa univ A Ο:= fun x => (fe x.1, fa x.2): β Γ β β u Γ v x: u Γ v hx1: x.1 β E hx2: x.2 β A e: β leftβΒΉ: e β univ hfe: fe e = x.1 a: β leftβ: a β univ hfa: fa a = x.2
h
Ο (e, a) = x
u, v: Type E: Set u A: Set v fe: β β u fe_surj: SurjOn fe univ E fa: β β v fa_surj: SurjOn fa univ A Ο:= fun x => (fe x.1, fa x.2): β Γ β β u Γ v x: u Γ v hx1: x.1 β E hx2: x.2 β A e: β leftβΒΉ: e β univ hfe: fe e = x.1 a: β leftβ: a β univ hfa: fa a = x.2
h
(x.1, fa a) = x
u, v: Type E: Set u A: Set v fe: β β u fe_surj: SurjOn fe univ E fa: β β v fa_surj: SurjOn fa univ A Ο:= fun x => (fe x.1, fa x.2): β Γ β β u Γ v x: u Γ v hx1: x.1 β E hx2: x.2 β A e: β leftβΒΉ: e β univ hfe: fe e = x.1 a: β leftβ: a β univ hfa: fa a = x.2
h
Ο (e, a) = x
u, v: Type E: Set u A: Set v fe: β β u fe_surj: SurjOn fe univ E fa: β β v fa_surj: SurjOn fa univ A Ο:= fun x => (fe x.1, fa x.2): β Γ β β u Γ v x: u Γ v hx1: x.1 β E hx2: x.2 β A e: β leftβΒΉ: e β univ hfe: fe e = x.1 a: β leftβ: a β univ hfa: fa a = x.2
h
(x.1, x.2) = x
Goals accomplished!π
Goals accomplished!π
u, v: Type E: Set u A: Set v he: countable E ha: countable A
countable {x | x.1 β E β§ x.2 β A}
Goals accomplished!π
/--β is countable. (Example 1 p.3)-/lemma Q_countable : countable (univ : Set β) :=
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β
countable univ
countable univ
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β
countable univ
Goals accomplished!π
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β
SurjOn f A univ
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β
SurjOn f A univ
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β
SurjOn f A univ
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β q: β aβ: q β univ
q β f '' A
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β
SurjOn f A univ
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β q: β aβ: q β univ x:= (q.num, q.den): β€ Γ β
q β f '' A
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β
SurjOn f A univ
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β q: β aβ: q β univ x:= (q.num, q.den): β€ Γ β
h
x β A β§ f x = q
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β
SurjOn f A univ
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β q: β aβ: q β univ x:= (q.num, q.den): β€ Γ β
h
f x = q
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β
SurjOn f A univ
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β q: β aβ: q β univ x:= (q.num, q.den): β€ Γ β
h
f x = q
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β q: β aβ: q β univ x:= (q.num, q.den): β€ Γ β
h
f x = q
Goals accomplished!π
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β q: β aβ: q β univ x:= (q.num, q.den): β€ Γ β
h
(if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0) = q
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β
SurjOn f A univ
[Meta.Tactic.simp.rewrite] dif_pos:1000, if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― }
else0==> { num := x.1, den := x.2, den_nz := β―, reduced := β― }
[Meta.Tactic.simp.rewrite] dif_neg:1000, if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― }
else0==>0
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β q: β aβ: q β univ x:= (q.num, q.den): β€ Γ β hβ: x β A
h.isTrue
{ num := x.1, den := x.2, den_nz := β―, reduced := β― } = q
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β q: β aβ: q β univ x:= (q.num, q.den): β€ Γ β hβ: x β A
0= q
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β
SurjOn f A univ
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β q: β aβ: q β univ x:= (q.num, q.den): β€ Γ β hβ: x β A
h.isTrue
{ num := x.1, den := x.2, den_nz := β―, reduced := β― } = q
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β q: β aβ: q β univ x:= (q.num, q.den): β€ Γ β hβ: x β A
h.isTrue
{ num := x.1, den := x.2, den_nz := β―, reduced := β― } = q
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β q: β aβ: q β univ x:= (q.num, q.den): β€ Γ β hβ: x β A
0= q
Goals accomplished!π
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β
SurjOn f A univ
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β q: β aβ: q β univ x:= (q.num, q.den): β€ Γ β hβ: x β A
h.isFalse
0= q
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β q: β aβ: q β univ x:= (q.num, q.den): β€ Γ β h_if: x β A
False
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β q: β aβ: q β univ x:= (q.num, q.den): β€ Γ β h_if: x β A
0= q
Goals accomplished!π
Goals accomplished!π
countable univ
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β f_surj: SurjOn f A univ
countable univ
Goals accomplished!π
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β f_surj: SurjOn f A univ
countable univ
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β f_surj: SurjOn f A univ
countable univ
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β f_surj: SurjOn f A univ
countable univ
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β f_surj: SurjOn f A univ
countable univ
Goals accomplished!π
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β f_surj: SurjOn f A univ
{x | x.1 β univ β§ x.2 β univ} = univ
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β f_surj: SurjOn f A univ
{x | x.1 β univ β§ x.2 β univ} = univ
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β f_surj: SurjOn f A univ
{x | x.1 β univ β§ x.2 β univ} = univ
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β f_surj: SurjOn f A univ x: β€ Γ β
h
x β {x | x.1 β univ β§ x.2 β univ} β x β univ
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β f_surj: SurjOn f A univ
{x | x.1 β univ β§ x.2 β univ} = univ
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β f_surj: SurjOn f A univ x: β€ Γ β
h.mp
x β {x | x.1 β univ β§ x.2 β univ} β x β univ
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β f_surj: SurjOn f A univ x: β€ Γ β
x β univ β x β {x | x.1 β univ β§ x.2 β univ}
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β f_surj: SurjOn f A univ
{x | x.1 β univ β§ x.2 β univ} = univ
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β f_surj: SurjOn f A univ x: β€ Γ β
h.mp
x β {x | x.1 β univ β§ x.2 β univ} β x β univ
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β f_surj: SurjOn f A univ x: β€ Γ β
h.mp
x β {x | x.1 β univ β§ x.2 β univ} β x β univ
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β f_surj: SurjOn f A univ x: β€ Γ β
x β univ β x β {x | x.1 β univ β§ x.2 β univ}
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β f_surj: SurjOn f A univ x: β€ Γ β aβ: x β {x | x.1 β univ β§ x.2 β univ}
h.mp
x β univ
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β f_surj: SurjOn f A univ x: β€ Γ β
h.mp
x β {x | x.1 β univ β§ x.2 β univ} β x β univ
Goals accomplished!π
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β f_surj: SurjOn f A univ
{x | x.1 β univ β§ x.2 β univ} = univ
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β f_surj: SurjOn f A univ x: β€ Γ β aβ: x β univ
h.mpr
x β {x | x.1 β univ β§ x.2 β univ}
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β f_surj: SurjOn f A univ
{x | x.1 β univ β§ x.2 β univ} = univ
Goals accomplished!π
Goals accomplished!π
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β f_surj: SurjOn f A univ
countable univ
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β f_surj: SurjOn f A univ eq_set: {x | x.1 β univ β§ x.2 β univ} = univ univ_countable: countable {x | x.1 β univ β§ x.2 β univ}
countable univ
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β f_surj: SurjOn f A univ
countable univ
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β f_surj: SurjOn f A univ eq_set: {x | x.1 β univ β§ x.2 β univ} = univ univ_countable: countable {x | x.1 β univ β§ x.2 β univ}
countable univ
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β f_surj: SurjOn f A univ eq_set: {x | x.1 β univ β§ x.2 β univ} = univ univ_countable: countable univ
countable univ
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β f_surj: SurjOn f A univ eq_set: {x | x.1 β univ β§ x.2 β univ} = univ univ_countable: countable univ
countable univ
Goals accomplished!π
Goals accomplished!π
countable univ
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β f_surj: SurjOn f A univ countable_prod: countable univ
countable univ
Goals accomplished!π
A:= {x |0< x.2 β§ x.1.natAbs.Coprime x.2}: Set (β€ Γ β) f:= fun x =>if h : x β A then { num := x.1, den := x.2, den_nz := β―, reduced := β― } else0: β€ Γ β β β f_surj: SurjOn f A univ countable_prod: countable univ countable_A: countable A
countable univ
countable univ
Goals accomplished!π
/--Let A and E two sets such that E is uncountable. If it exists a surjection from A to E, then A is uncountable.-/lemma uncountable_trans {u v : Type} (A : Set u) {E : Set v} (h : Β¬countable E) : (β (f : u β v), SurjOn f A E) βΒ¬countable A :=
Goals accomplished!π
u, v: Type A: Set u E: Set v h: Β¬countable E
(β f, SurjOn f A E) βΒ¬countable A
u, v: Type A: Set u E: Set v h: Β¬countable E exists_surj: β f, SurjOn f A E
Β¬countable A
u, v: Type A: Set u E: Set v h: Β¬countable E
(β f, SurjOn f A E) βΒ¬countable A
u, v: Type A: Set u E: Set v h: Β¬countable E f: u β v f_surj: SurjOn f A E
intro
Β¬countable A
u, v: Type A: Set u E: Set v h: Β¬countable E
(β f, SurjOn f A E) βΒ¬countable A
u, v: Type A: Set u E: Set v h: Β¬countable E f: u β v f_surj: SurjOn f A E h_countable: countable A
intro
False
u, v: Type A: Set u E: Set v h: Β¬countable E
(β f, SurjOn f A E) βΒ¬countable A
u, v: Type A: Set u E: Set v h: Β¬countable E f: u β v f_surj: SurjOn f A E g: β β u g_surj: SurjOn g univ A
intro.intro
False
u, v: Type A: Set u E: Set v h: Β¬countable E
(β f, SurjOn f A E) βΒ¬countable A
u, v: Type A: Set u E: Set v h: Β¬countable E f: u β v f_surj: SurjOn f A E g: β β u g_surj: SurjOn g univ A
intro.intro
False
Goals accomplished!π
u, v: Type A: Set u E: Set v h: Β¬countable E f: u β v f_surj: SurjOn f A E g: β β u g_surj: SurjOn g univ A
SurjOn (f β g) univ E
u, v: Type A: Set u E: Set v h: Β¬countable E f: u β v f_surj: SurjOn f A E g: β β u g_surj: SurjOn g univ A
SurjOn (f β g) univ E
u, v: Type A: Set u E: Set v h: Β¬countable E f: u β v f_surj: SurjOn f A E g: β β u g_surj: SurjOn g univ A
SurjOn (f β g) univ E
u, v: Type A: Set u E: Set v h: Β¬countable E f: u β v f_surj: SurjOn f A E g: β β u g_surj: SurjOn g univ A e: v e_in_E: e β E
e β f β g '' univ
u, v: Type A: Set u E: Set v h: Β¬countable E f: u β v f_surj: SurjOn f A E g: β β u g_surj: SurjOn g univ A
SurjOn (f β g) univ E
u, v: Type A: Set u E: Set v h: Β¬countable E f: u β v f_surj: SurjOn f A E g: β β u g_surj: SurjOn g univ A e: v e_in_E: e β E a: u a_in_A: a β A fa: f a = e
intro.intro
e β f β g '' univ
u, v: Type A: Set u E: Set v h: Β¬countable E f: u β v f_surj: SurjOn f A E g: β β u g_surj: SurjOn g univ A
SurjOn (f β g) univ E
u, v: Type A: Set u E: Set v h: Β¬countable E f: u β v f_surj: SurjOn f A E g: β β u g_surj: SurjOn g univ A e: v e_in_E: e β E a: u a_in_A: a β A fa: f a = e n: β n_in_N: n β univ gn: g n = a
intro.intro.intro.intro
e β f β g '' univ
u, v: Type A: Set u E: Set v h: Β¬countable E f: u β v f_surj: SurjOn f A E g: β β u g_surj: SurjOn g univ A
SurjOn (f β g) univ E
u, v: Type A: Set u E: Set v h: Β¬countable E f: u β v f_surj: SurjOn f A E g: β β u g_surj: SurjOn g univ A e: v e_in_E: e β E a: u a_in_A: a β A fa: f a = e n: β n_in_N: n β univ gn: g n = a
right
(f β g) n = e
u, v: Type A: Set u E: Set v h: Β¬countable E f: u β v f_surj: SurjOn f A E g: β β u g_surj: SurjOn g univ A
SurjOn (f β g) univ E
u, v: Type A: Set u E: Set v h: Β¬countable E f: u β v f_surj: SurjOn f A E g: β β u g_surj: SurjOn g univ A e: v e_in_E: e β E a: u a_in_A: a β A fa: f a = e n: β n_in_N: n β univ gn: g n = a
right
(f β g) n = e
u, v: Type A: Set u E: Set v h: Β¬countable E f: u β v f_surj: SurjOn f A E g: β β u g_surj: SurjOn g univ A e: v e_in_E: e β E a: u a_in_A: a β A fa: f a = e n: β n_in_N: n β univ gn: g n = a
right
(f β g) n = e
Goals accomplished!π
u, v: Type A: Set u E: Set v h: Β¬countable E f: u β v f_surj: SurjOn f A E g: β β u g_surj: SurjOn g univ A e: v e_in_E: e β E a: u a_in_A: a β A fa: f a = e n: β n_in_N: n β univ gn: g n = a
right
f (g n) = e
u, v: Type A: Set u E: Set v h: Β¬countable E f: u β v f_surj: SurjOn f A E g: β β u g_surj: SurjOn g univ A e: v e_in_E: e β E a: u a_in_A: a β A fa: f a = e n: β n_in_N: n β univ gn: g n = a
right
(f β g) n = e
u, v: Type A: Set u E: Set v h: Β¬countable E f: u β v f_surj: SurjOn f A E g: β β u g_surj: SurjOn g univ A e: v e_in_E: e β E a: u a_in_A: a β A fa: f a = e n: β n_in_N: n β univ gn: g n = a
right
f a = e
u, v: Type A: Set u E: Set v h: Β¬countable E f: u β v f_surj: SurjOn f A E g: β β u g_surj: SurjOn g univ A e: v e_in_E: e β E a: u a_in_A: a β A fa: f a = e n: β n_in_N: n β univ gn: g n = a
right
f a = e
Goals accomplished!π
u, v: Type A: Set u E: Set v h: Β¬countable E
(β f, SurjOn f A E) βΒ¬countable A
u, v: Type A: Set u E: Set v h: Β¬countable E f: u β v f_surj: SurjOn f A E g: β β u g_surj: SurjOn g univ A fg_surj_N_E: SurjOn (f β g) univ E
intro.intro
False
Goals accomplished!π
u, v: Type A: Set u E: Set v h: Β¬countable E f: u β v f_surj: SurjOn f A E g: β β u g_surj: SurjOn g univ A fg_surj_N_E: SurjOn (f β g) univ E
intro.intro
False
Goals accomplished!π
u, v: Type A: Set u E: Set v h: Β¬countable E
(β f, SurjOn f A E) βΒ¬countable A
Goals accomplished!π
/--Corrolary: if A β E is uncountable, then E is uncountable.-/lemma subset_of_uncountable_set {u : Type} {E A : Set u} (h : A β E) (uncountable : Β¬ countable A) : Β¬ countable E :=
Goals accomplished!π
u: Type E, A: Set u h: A β E uncountable: Β¬countable A
Β¬countable E
u: Type E, A: Set u h: A β E uncountable: Β¬countable A h_contr: countable E
False
u: Type E, A: Set u h: A β E uncountable: Β¬countable A
Β¬countable E
u: Type E, A: Set u h: A β E uncountable: Β¬countable A h_contr: countable E f:= fun e => e: u β u
False
u: Type E, A: Set u h: A β E uncountable: Β¬countable A
Β¬countable E
u: Type E, A: Set u h: A β E uncountable: Β¬countable A h_contr: countable E f:= fun e => e: u β u f_surj: SurjOn f E A
False
u: Type E, A: Set u h: A β E uncountable: Β¬countable A
Β¬countable E
Goals accomplished!π
------------------------------FORMALIZATION-----------------------------------/--The power set of β is uncountable. (Example 4 p.3)-/lemma powerset_N_uncountable : Β¬countable (π« (univ : Set β)) :=
Goals accomplished!π
Β¬countable (π« univ)
h: countable (π« univ)
False
Β¬countable (π« univ)
Ο: β β Set β h: SurjOn Ο univ (π« univ)
intro
False
Β¬countable (π« univ)
Ο: β β Set β h: SurjOn Ο univ (π« univ) A:= {n | n β Ο n}: Set β
intro
False
Β¬countable (π« univ)
Ο: β β Set β A:= {n | n β Ο n}: Set β h: A β Ο '' univ
intro
False
Β¬countable (π« univ)
Ο: β β Set β A:= {n | n β Ο n}: Set β a: β leftβ: a β univ ha: Ο a = A
intro.intro.intro
False
Β¬countable (π« univ)
Ο: β β Set β A:= {n | n β Ο n}: Set β a: β leftβ: a β univ ha: Ο a = A ain: a β A
pos
False
Ο: β β Set β A:= {n | n β Ο n}: Set β a: β leftβ: a β univ ha: Ο a = A ain: Β¬a β A
False
Β¬countable (π« univ)
Ο: β β Set β A:= {n | n β Ο n}: Set β a: β leftβ: a β univ ha: Ο a = A ain: a β A
pos
False
Ο: β β Set β A:= {n | n β Ο n}: Set β a: β leftβ: a β univ ha: Ο a = A ain: a β A
pos
False
Ο: β β Set β A:= {n | n β Ο n}: Set β a: β leftβ: a β univ ha: Ο a = A ain: Β¬a β A
False
Ο: β β Set β A:= {n | n β Ο n}: Set β a: β leftβ: a β univ ha: Ο a = A ain: a β A a_in_phi: Β¬a β Ο a
pos
False
Ο: β β Set β A:= {n | n β Ο n}: Set β a: β leftβ: a β univ ha: Ο a = A ain: a β A
pos
False
Ο: β β Set β A:= {n | n β Ο n}: Set β a: β leftβ: a β univ ha: Ο a = A ain: a β A a_in_phi: a β Ο a
pos
False
Ο: β β Set β A:= {n | n β Ο n}: Set β a: β leftβ: a β univ ha: Ο a = A ain: a β A
pos
False
Ο: β β Set β A:= {n | n β Ο n}: Set β a: β leftβ: a β univ ha: Ο a = A ain: a β A a_in_phi: a β Ο a
pos
False
Ο: β β Set β A:= {n | n β Ο n}: Set β a: β leftβ: a β univ ha: Ο a = A ain: a β A a_in_phi: a β A
pos
False
Ο: β β Set β A:= {n | n β Ο n}: Set β a: β leftβ: a β univ ha: Ο a = A ain: a β A a_in_phi: a β A
pos
False
Ο: β β Set β A:= {n | n β Ο n}: Set β a: β leftβ: a β univ ha: Ο a = A ain: a β A a_in_phi: a β A
pos
False
Ο: β β Set β A:= {n | n β Ο n}: Set β a: β leftβ: a β univ ha: Ο a = A ain: a β A
pos
False
Goals accomplished!π
Β¬countable (π« univ)
Ο: β β Set β A:= {n | n β Ο n}: Set β a: β leftβ: a β univ ha: Ο a = A ain: a β A
neg
False
Β¬countable (π« univ)
Ο: β β Set β A:= {n | n β Ο n}: Set β a: β leftβ: a β univ ha: Ο a = A ain: a β A a_notin_phi_a: a β Ο a
neg
False
Β¬countable (π« univ)
Ο: β β Set β A:= {n | n β Ο n}: Set β a: β leftβ: a β univ ha: Ο a = A ain: a β A a_notin_phi_a: a β Ο a
neg
False
Ο: β β Set β A:= {n | n β Ο n}: Set β a: β leftβ: a β univ ha: Ο a = A ain: a β A a_notin_phi_a: a β A
neg
False
Ο: β β Set β A:= {n | n β Ο n}: Set β a: β leftβ: a β univ ha: Ο a = A ain: a β A a_notin_phi_a: a β A
neg
False
Ο: β β Set β A:= {n | n β Ο n}: Set β a: β leftβ: a β univ ha: Ο a = A ain: a β A a_notin_phi_a: a β A
neg
False
Β¬countable (π« univ)
Goals accomplished!π
/-- The set of all sequences in {0, 1}-/def zero_one := {u: β β β |βn, u n =0β¨ u n =1}
/--The set of all sequences in {0, 1} is uncountable. (Example 5 p.3)-/lemma zero_one_uncountable : Β¬countable zero_one :=
Goals accomplished!π
Β¬countable zero_one
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β
Β¬countable zero_one
Β¬countable zero_one
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β
Β¬countable zero_one
Goals accomplished!π
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β
SurjOn f zero_one (π« univ)
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β
SurjOn f zero_one (π« univ)
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β
SurjOn f zero_one (π« univ)
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ
A β f '' zero_one
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β
SurjOn f zero_one (π« univ)
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β
A β f '' zero_one
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β
SurjOn f zero_one (π« univ)
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β
h
Ο β zero_one β§ f Ο = A
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β
SurjOn f zero_one (π« univ)
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β
h
Ο β zero_one β§ f Ο = A
Goals accomplished!π
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β
Ο β zero_one
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β
Ο β zero_one
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β
Ο β zero_one
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β n: β
Ο n =0β¨ Ο n =1
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β
Ο β zero_one
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β n: β h: n β A
pos
Ο n =0β¨ Ο n =1
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β n: β h: n β A
Ο n =0β¨ Ο n =1
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β
Ο β zero_one
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β n: β h: n β A
pos
Ο n =0β¨ Ο n =1
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β n: β h: n β A
pos
Ο n =0β¨ Ο n =1
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β n: β h: n β A
Ο n =0β¨ Ο n =1
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β n: β h: n β A
pos
Ο n =0β¨ Ο n =1
Goals accomplished!π
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β n: β h: n β A
Ο n =1
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β n: β h: n β A
Ο n =1
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β n: β h: n β A
Ο n =1
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β n: β h: n β A
Ο n =1
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β n: β h: n β A
n β A β1=0
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β n: β h: n β A
n β A β1=0
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β n: β h: n β A
Ο n =1
Goals accomplished!π
Goals accomplished!π
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β n: β h: n β A
pos
Ο n =0β¨ Ο n =1
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β n: β h: n β A ind_eq_1: Ο n =1
pos.h
Ο n =1
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β n: β h: n β A ind_eq_1: Ο n =1
pos.h
Ο n =1
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β n: β h: n β A
pos
Ο n =0β¨ Ο n =1
Goals accomplished!π
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β
Ο β zero_one
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β n: β h: n β A
neg
Ο n =0β¨ Ο n =1
Goals accomplished!π
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β n: β h: n β A
Ο n =0
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β n: β h: n β A
Ο n =0
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β n: β h: n β A
Ο n =0
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β n: β h: n β A
Ο n =0
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β n: β h: n β A
n β A β1=0
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β n: β h: n β A
n β A β1=0
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β n: β h: n β A
Ο n =0
Goals accomplished!π
Goals accomplished!π
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β
Ο β zero_one
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β n: β h: n β A ind_eq_0: Ο n =0
neg.h
Ο n =0
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β n: β h: n β A ind_eq_0: Ο n =0
neg.h
Ο n =0
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β
Ο β zero_one
Goals accomplished!π
Goals accomplished!π
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β
SurjOn f zero_one (π« univ)
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β Ο_in_zero_one: Ο β zero_one
h
f Ο = A
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β
SurjOn f zero_one (π« univ)
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β Ο_in_zero_one: Ο β zero_one n: β
h.h
n β f Ο β n β A
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β
SurjOn f zero_one (π« univ)
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β Ο_in_zero_one: Ο β zero_one n: β
h.h.mp
n β f Ο β n β A
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β Ο_in_zero_one: Ο β zero_one n: β
n β A β n β f Ο
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β
SurjOn f zero_one (π« univ)
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β Ο_in_zero_one: Ο β zero_one n: β
h.h.mp
n β f Ο β n β A
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β Ο_in_zero_one: Ο β zero_one n: β
h.h.mp
n β f Ο β n β A
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β Ο_in_zero_one: Ο β zero_one n: β
n β A β n β f Ο
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β Ο_in_zero_one: Ο β zero_one n: β n_in_f_Ο: n β f Ο
h.h.mp
n β A
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β Ο_in_zero_one: Ο β zero_one n: β
h.h.mp
n β f Ο β n β A
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β Ο_in_zero_one: Ο β zero_one n: β n_in_f_Ο: n β f Ο Οn_eq_1: Ο n =1
h.h.mp
n β A
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β Ο_in_zero_one: Ο β zero_one n: β
h.h.mp
n β f Ο β n β A
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β Ο_in_zero_one: Ο β zero_one n: β n_in_f_Ο: n β f Ο Οn_eq_1: Ο n =1
h.h.mp
n β A
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β Ο_in_zero_one: Ο β zero_one n: β n_in_f_Ο: n β f Ο Οn_eq_1: n β A β1=0
h.h.mp
n β A
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β Ο_in_zero_one: Ο β zero_one n: β n_in_f_Ο: n β f Ο Οn_eq_1: n β A β1=0
h.h.mp
n β A
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β Ο_in_zero_one: Ο β zero_one n: β n_in_f_Ο: n β f Ο Οn_eq_1: n β A β1=0
h.h.mp
n β A
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β Ο_in_zero_one: Ο β zero_one n: β
h.h.mp
n β f Ο β n β A
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β Ο_in_zero_one: Ο β zero_one n: β n_in_f_Ο: n β f Ο Οn_eq_1: n β A β1=0 n_notin_A: Β¬n β A
h.h.mp
False
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β Ο_in_zero_one: Ο β zero_one n: β
h.h.mp
n β f Ο β n β A
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β Ο_in_zero_one: Ο β zero_one n: β n_in_f_Ο: n β f Ο n_notin_A: Β¬n β A Οn_eq_1: 1=0
h.h.mp
False
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β Ο_in_zero_one: Ο β zero_one n: β
h.h.mp
n β f Ο β n β A
Goals accomplished!π
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β
SurjOn f zero_one (π« univ)
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β Ο_in_zero_one: Ο β zero_one n: β n_in_A: n β A
h.h.mpr
n β f Ο
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β
SurjOn f zero_one (π« univ)
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β Ο_in_zero_one: Ο β zero_one n: β n_in_A: n β A
h.h.mpr
n β f Ο
Goals accomplished!π
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β Ο_in_zero_one: Ο β zero_one n: β n_in_A: n β A
Ο n =1
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β Ο_in_zero_one: Ο β zero_one n: β n_in_A: n β A
Ο n =1
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β Ο_in_zero_one: Ο β zero_one n: β n_in_A: n β A
Ο n =1
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β Ο_in_zero_one: Ο β zero_one n: β n_in_A: n β A
Ο n =1
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β Ο_in_zero_one: Ο β zero_one n: β n_in_A: n β A
n β A β1=0
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β Ο_in_zero_one: Ο β zero_one n: β n_in_A: n β A
n β A β1=0
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β Ο_in_zero_one: Ο β zero_one n: β n_in_A: n β A
Ο n =1
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β Ο_in_zero_one: Ο β zero_one n: β n_in_A: n β A n_notin_A: n β A
1=0
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β A: Set β aβ: A βπ« univ Ο:= A.indicator fun x =>1: β β β Ο_in_zero_one: Ο β zero_one n: β n_in_A: n β A
Ο n =1
Goals accomplished!π
Goals accomplished!π
f:= fun Ο => {n | Ο n =1}: (β β β) β Set β
SurjOn f zero_one (π« univ)
Goals accomplished!π
Goals accomplished!π
Β¬countable zero_one
Goals accomplished!π
/--The set of all sequences to β is uncountable.-/example : Β¬ countable (univ : Set (β β β)) :=
subset_of_uncountable_set (Ξ» _ _ β¦ trivial) zero_one_uncountable
/--For any real number x and any positive number Ξ΅, it exists a rational q such that |x - q| < Ξ΅.-/lemma Q_dense (x : β) : β Ξ΅ >0, β (q : β), |x - q|< Ξ΅ :=
Goals accomplished!π
x: β
β Ξ΅ >0, β q, |x -βq|< Ξ΅
x, Ξ΅: β Ξ΅_pos: Ξ΅ >0
β q, |x -βq|< Ξ΅
x: β
β Ξ΅ >0, β q, |x -βq|< Ξ΅
x, Ξ΅: β Ξ΅_pos: Ξ΅ >0
β q, |x -βq|< Ξ΅
Goals accomplished!π
x, Ξ΅: β Ξ΅_pos: Ξ΅ >0
β q, |x -βq|< Ξ΅
Goals accomplished!π
x: β
β Ξ΅ >0, β q, |x -βq|< Ξ΅
x, Ξ΅: β Ξ΅_pos: Ξ΅ >0 h: x < x + Ξ΅ q: β hql: x <βq hqr: βq < x + Ξ΅
intro.intro
β q, |x -βq|< Ξ΅
x: β
β Ξ΅ >0, β q, |x -βq|< Ξ΅
x, Ξ΅: β Ξ΅_pos: Ξ΅ >0 h: x < x + Ξ΅ q: β hql: x <βq hqr: βq < x + Ξ΅
h
|x -βq|< Ξ΅
x: β
β Ξ΅ >0, β q, |x -βq|< Ξ΅
x, Ξ΅: β Ξ΅_pos: Ξ΅ >0 h: x < x + Ξ΅ q: β hql: x <βq hqr: βq < x + Ξ΅
h
|x -βq|< Ξ΅
Warning: unused variable`x_minus_q_neg`
note: this linter can be disabled with`set_option linter.unusedVariables false`
x, Ξ΅: β Ξ΅_pos: Ξ΅ >0 h: x < x + Ξ΅ q: β hql: x <βq hqr: βq < x + Ξ΅
h
|x -βq|< Ξ΅
x, Ξ΅: β Ξ΅_pos: Ξ΅ >0 h: x < x + Ξ΅ q: β hql: x <βq hqr: βq < x + Ξ΅
h
|x -βq|< Ξ΅
Goals accomplished!π
x, Ξ΅: β Ξ΅_pos: Ξ΅ >0 h: x < x + Ξ΅ q: β hql: x <βq hqr: βq < x + Ξ΅
h
|x -βq|< Ξ΅
Goals accomplished!π
x: β
β Ξ΅ >0, β q, |x -βq|< Ξ΅
x, Ξ΅: β Ξ΅_pos: Ξ΅ >0 h: x < x + Ξ΅ q: β hql: x <βq hqr: βq < x + Ξ΅ x_minus_q_neg: x -βq <0
h
|x -βq|< Ξ΅
Goals accomplished!π
x, Ξ΅: β Ξ΅_pos: Ξ΅ >0 h: x < x + Ξ΅ q: β hql: x <βq hqr: βq < x + Ξ΅ x_minus_q_neg: x -βq <0
|x -βq|=-(x -βq)
x, Ξ΅: β Ξ΅_pos: Ξ΅ >0 h: x < x + Ξ΅ q: β hql: x <βq hqr: βq < x + Ξ΅ x_minus_q_neg: x -βq <0
|x -βq|=-(x -βq)
x, Ξ΅: β Ξ΅_pos: Ξ΅ >0 h: x < x + Ξ΅ q: β hql: x <βq hqr: βq < x + Ξ΅ x_minus_q_neg: x -βq <0
|x -βq|=-(x -βq)
x, Ξ΅: β Ξ΅_pos: Ξ΅ >0 h: x < x + Ξ΅ q: β hql: x <βq hqr: βq < x + Ξ΅ x_minus_q_neg: x -βq <0
|x -βq|=-(x -βq)
x, Ξ΅: β Ξ΅_pos: Ξ΅ >0 h: x < x + Ξ΅ q: β hql: x <βq hqr: βq < x + Ξ΅ x_minus_q_neg: x -βq <0
x -βq β€0
x, Ξ΅: β Ξ΅_pos: Ξ΅ >0 h: x < x + Ξ΅ q: β hql: x <βq hqr: βq < x + Ξ΅ x_minus_q_neg: x -βq <0
x -βq β€0
x, Ξ΅: β Ξ΅_pos: Ξ΅ >0 h: x < x + Ξ΅ q: β hql: x <βq hqr: βq < x + Ξ΅ x_minus_q_neg: x -βq <0
|x -βq|=-(x -βq)
Goals accomplished!π
Goals accomplished!π
x: β
β Ξ΅ >0, β q, |x -βq|< Ξ΅
x, Ξ΅: β Ξ΅_pos: Ξ΅ >0 h: x < x + Ξ΅ q: β hql: x <βq hqr: βq < x + Ξ΅ x_minus_q_neg: x -βq <0 abs_eq_neg: |x -βq|=-(x -βq)
h
|x -βq|< Ξ΅
x, Ξ΅: β Ξ΅_pos: Ξ΅ >0 h: x < x + Ξ΅ q: β hql: x <βq hqr: βq < x + Ξ΅ x_minus_q_neg: x -βq <0 abs_eq_neg: |x -βq|=-(x -βq)
h
-(x -βq) < Ξ΅
x, Ξ΅: β Ξ΅_pos: Ξ΅ >0 h: x < x + Ξ΅ q: β hql: x <βq hqr: βq < x + Ξ΅ x_minus_q_neg: x -βq <0 abs_eq_neg: |x -βq|=-(x -βq)
h
|x -βq|< Ξ΅
x, Ξ΅: β Ξ΅_pos: Ξ΅ >0 h: x < x + Ξ΅ q: β hql: x <βq hqr: βq < x + Ξ΅ x_minus_q_neg: x -βq <0 abs_eq_neg: |x -βq|=-(x -βq)
h
-(x -βq) < Ξ΅
Goals accomplished!π
x, Ξ΅: β Ξ΅_pos: Ξ΅ >0 h: x < x + Ξ΅ q: β hql: x <βq hqr: βq < x + Ξ΅ x_minus_q_neg: x -βq <0 abs_eq_neg: |x -βq|=-(x -βq)
h
βq - x < Ξ΅
x: β
β Ξ΅ >0, β q, |x -βq|< Ξ΅
Goals accomplished!π
/--For any real number x, it exists a sequence of rational that tends to x.-/example (x : β) : β (u : β β β), Tendsto (Ξ» n β¦ ((u n) : β)) atTop (π x) :=
Goals accomplished!π
x: β
β u, Tendsto (fun n =>β(u n)) atTop (π x)
x: β A:= fun n => {q ||x -βq|<1/ (βn +1)}: β β Set β
β u, Tendsto (fun n =>β(u n)) atTop (π x)
x: β
β u, Tendsto (fun n =>β(u n)) atTop (π x)
x: β A:= fun n => {q ||x -βq|<1/ (βn +1)}: β β Set β
β u, Tendsto (fun n =>β(u n)) atTop (π x)
Goals accomplished!π
x: β A:= fun n => {q ||x -βq|<1/ (βn +1)}: β β Set β
β (n : β), (A n).Nonempty
x: β A:= fun n => {q ||x -βq|<1/ (βn +1)}: β β Set β
β (n : β), (A n).Nonempty
x: β A:= fun n => {q ||x -βq|<1/ (βn +1)}: β β Set β
β (n : β), (A n).Nonempty
x: β A:= fun n => {q ||x -βq|<1/ (βn +1)}: β β Set β n: β
(A n).Nonempty
x: β A:= fun n => {q ||x -βq|<1/ (βn +1)}: β β Set β
β (n : β), (A n).Nonempty
x: β A:= fun n => {q ||x -βq|<1/ (βn +1)}: β β Set β n: β q: β hq: |x -βq|<1/ (βn +1)
intro
(A n).Nonempty
x: β A:= fun n => {q ||x -βq|<1/ (βn +1)}: β β Set β
β (n : β), (A n).Nonempty
Goals accomplished!π
Goals accomplished!π
x: β
β u, Tendsto (fun n =>β(u n)) atTop (π x)
x: β A:= fun n => {q ||x -βq|<1/ (βn +1)}: β β Set β non_empty: β (n : β), (A n).Nonempty u:= fun n =>β―.some: β β β
β u, Tendsto (fun n =>β(u n)) atTop (π x)
x: β
β u, Tendsto (fun n =>β(u n)) atTop (π x)
x: β A:= fun n => {q ||x -βq|<1/ (βn +1)}: β β Set β non_empty: β (n : β), (A n).Nonempty u:= fun n =>β―.some: β β β
h
Tendsto (fun n =>β(u n)) atTop (π x)
x: β
β u, Tendsto (fun n =>β(u n)) atTop (π x)
x: β A:= fun n => {q ||x -βq|<1/ (βn +1)}: β β Set β non_empty: β (n : β), (A n).Nonempty u:= fun n =>β―.some: β β β
h
Tendsto (fun n =>β(u n)) atTop (π x)
x: β A:= fun n => {q ||x -βq|<1/ (βn +1)}: β β Set β non_empty: β (n : β), (A n).Nonempty u:= fun n =>β―.some: β β β
h
β Ξ΅ >0, β N, β n > N, dist (β(u n)) x < Ξ΅
x: β A:= fun n => {q ||x -βq|<1/ (βn +1)}: β β Set β non_empty: β (n : β), (A n).Nonempty u:= fun n =>β―.some: β β β
h
β Ξ΅ >0, β N, β n > N, dist (β(u n)) x < Ξ΅
x: β
β u, Tendsto (fun n =>β(u n)) atTop (π x)
x: β A:= fun n => {q ||x -βq|<1/ (βn +1)}: β β Set β non_empty: β (n : β), (A n).Nonempty u:= fun n =>β―.some: β β β dst: β (n : β), dist (β(u n)) x =|x -β(u n)|
h
β Ξ΅ >0, β N, β n > N, dist (β(u n)) x < Ξ΅
x: β
β u, Tendsto (fun n =>β(u n)) atTop (π x)
x: β A:= fun n => {q ||x -βq|<1/ (βn +1)}: β β Set β non_empty: β (n : β), (A n).Nonempty u:= fun n =>β―.some: β β β dst: β (n : β), dist (β(u n)) x =|x -β(u n)|
h
β Ξ΅ >0, β N, β n > N, dist (β(u n)) x < Ξ΅
[Meta.Tactic.simp.rewrite] dst:1000, dist (β(u n)) x ==>|x -β(u n)|
x: β A:= fun n => {q ||x -βq|<1/ (βn +1)}: β β Set β non_empty: β (n : β), (A n).Nonempty u:= fun n =>β―.some: β β β dst: β (n : β), dist (β(u n)) x =|x -β(u n)|
h
β Ξ΅ >0, β N, β n > N, |x -β(u n)|< Ξ΅
x: β A:= fun n => {q ||x -βq|<1/ (βn +1)}: β β Set β non_empty: β (n : β), (A n).Nonempty u:= fun n =>β―.some: β β β dst: β (n : β), dist (β(u n)) x =|x -β(u n)|
h
β Ξ΅ >0, β N, β n > N, |x -β(u n)|< Ξ΅
x: β
β u, Tendsto (fun n =>β(u n)) atTop (π x)
x: β A:= fun n => {q ||x -βq|<1/ (βn +1)}: β β Set β non_empty: β (n : β), (A n).Nonempty u:= fun n =>β―.some: β β β dst: β (n : β), dist (β(u n)) x =|x -β(u n)| Ξ΅: β Ξ΅_pos: Ξ΅ >0
h
β N, β n > N, |x -β(u n)|< Ξ΅
x: β
β u, Tendsto (fun n =>β(u n)) atTop (π x)
x: β A:= fun n => {q ||x -βq|<1/ (βn +1)}: β β Set β non_empty: β (n : β), (A n).Nonempty u:= fun n =>β―.some: β β β dst: β (n : β), dist (β(u n)) x =|x -β(u n)| Ξ΅: β Ξ΅_pos: Ξ΅ >0
h
β N, β n > N, |x -β(u n)|< Ξ΅
Goals accomplished!π
x: β A:= fun n => {q ||x -βq|<1/ (βn +1)}: β β Set β non_empty: β (n : β), (A n).Nonempty u:= fun n =>β―.some: β β β dst: β (n : β), dist (β(u n)) x =|x -β(u n)| Ξ΅: β Ξ΅_pos: Ξ΅ >0
β N, 1/ (βN +1) < Ξ΅
x: β A:= fun n => {q ||x -βq|<1/ (βn +1)}: β β Set β non_empty: β (n : β), (A n).Nonempty u:= fun n =>β―.some: β β β dst: β (n : β), dist (β(u n)) x =|x -β(u n)| Ξ΅: β Ξ΅_pos: Ξ΅ >0
β N, 1/ (βN +1) < Ξ΅
x: β A:= fun n => {q ||x -βq|<1/ (βn +1)}: β β Set β non_empty: β (n : β), (A n).Nonempty u:= fun n =>β―.some: β β β dst: β (n : β), dist (β(u n)) x =|x -β(u n)| Ξ΅: β Ξ΅_pos: Ξ΅ >0
β N, 1/ (βN +1) < Ξ΅
x: β A:= fun n => {q ||x -βq|<1/ (βn +1)}: β β Set β non_empty: β (n : β), (A n).Nonempty u:= fun n =>β―.some: β β β dst: β (n : β), dist (β(u n)) x =|x -β(u n)| Ξ΅: β Ξ΅_pos: Ξ΅ >0
h
1/ (ββ1/ Ξ΅ββ+1) < Ξ΅
x: β A:= fun n => {q ||x -βq|<1/ (βn +1)}: β β Set β non_empty: β (n : β), (A n).Nonempty u:= fun n =>β―.some: β β β dst: β (n : β), dist (β(u n)) x =|x -β(u n)| Ξ΅: β Ξ΅_pos: Ξ΅ >0
β N, 1/ (βN +1) < Ξ΅
x: β A:= fun n => {q ||x -βq|<1/ (βn +1)}: β β Set β non_empty: β (n : β), (A n).Nonempty u:= fun n =>β―.some: β β β dst: β (n : β), dist (β(u n)) x =|x -β(u n)| Ξ΅: β Ξ΅_pos: Ξ΅ >0 R_pos: 0<ββ1/ Ξ΅ββ+1
h
1/ (ββ1/ Ξ΅ββ+1) < Ξ΅
x: β A:= fun n => {q ||x -βq|<1/ (βn +1)}: β β Set β non_empty: β (n : β), (A n).Nonempty u:= fun n =>β―.some: β β β dst: β (n : β), dist (β(u n)) x =|x -β(u n)| Ξ΅: β Ξ΅_pos: Ξ΅ >0
β N, 1/ (βN +1) < Ξ΅
x: β A:= fun n => {q ||x -βq|<1/ (βn +1)}: β β Set β non_empty: β (n : β), (A n).Nonempty u:= fun n =>β―.some: β β β dst: β (n : β), dist (β(u n)) x =|x -β(u n)| Ξ΅: β Ξ΅_pos: Ξ΅ >0 R_pos: 0<ββ1/ Ξ΅ββ+1
h
1/ (ββ1/ Ξ΅ββ+1) < Ξ΅
x: β A:= fun n => {q ||x -βq|<1/ (βn +1)}: β β Set β non_empty: β (n : β), (A n).Nonempty u:= fun n =>β―.some: β β β dst: β (n : β), dist (β(u n)) x =|x -β(u n)| Ξ΅: β Ξ΅_pos: Ξ΅ >0 R_pos: 0<ββ1/ Ξ΅ββ+1
h
1/ (ββ1/ Ξ΅ββ+1) < Ξ΅
Goals accomplished!π
x: β A:= fun n => {q ||x -βq|<1/ (βn +1)}: β β Set β non_empty: β (n : β), (A n).Nonempty u:= fun n =>β―.some: β β β dst: β (n : β), dist (β(u n)) x =|x -β(u n)| Ξ΅: β Ξ΅_pos: Ξ΅ >0 R_pos: 0<ββ1/ Ξ΅ββ+1
h
(ββ1/ Ξ΅ββ+1)β»ΒΉ< Ξ΅
x: β A:= fun n => {q ||x -βq|<1/ (βn +1)}: β β Set β non_empty: β (n : β), (A n).Nonempty u:= fun n =>β―.some: β β β dst: β (n : β), dist (β(u n)) x =|x -β(u n)| Ξ΅: β Ξ΅_pos: Ξ΅ >0
β N, 1/ (βN +1) < Ξ΅
x: β A:= fun n => {q ||x -βq|<1/ (βn +1)}: β β Set β non_empty: β (n : β), (A n).Nonempty u:= fun n =>β―.some: β β β dst: β (n : β), dist (β(u n)) x =|x -β(u n)| Ξ΅: β Ξ΅_pos: Ξ΅ >0 R_pos: 0<ββ1/ Ξ΅ββ+1
h
(ββ1/ Ξ΅ββ+1)β»ΒΉ< Ξ΅
Warning: `inv_lt` has been deprecated, use `inv_lt_commβ` instead
x: β A:= fun n => {q ||x -βq|<1/ (βn +1)}: β β Set β non_empty: β (n : β), (A n).Nonempty u:= fun n =>β―.some: β β β dst: β (n : β), dist (β(u n)) x =|x -β(u n)| Ξ΅: β Ξ΅_pos: Ξ΅ >0 R_pos: 0<ββ1/ Ξ΅ββ+1
h
(ββ1/ Ξ΅ββ+1)β»ΒΉ< Ξ΅
x: β A:= fun n => {q ||x -βq|<1/ (βn +1)}: β β Set β non_empty: β (n : β), (A n).Nonempty u:= fun n =>β―.some: β β β dst: β (n : β), dist (β(u n)) x =|x -β(u n)| Ξ΅: β Ξ΅_pos: Ξ΅ >0 R_pos: 0<ββ1/ Ξ΅ββ+1
h
Ξ΅β»ΒΉ<ββ1/ Ξ΅ββ+1
x: β A:= fun n => {q ||x -βq|<1/ (βn +1)}: β β Set β non_empty: β (n : β), (A n).Nonempty u:= fun n =>β―.some: β β β dst: β (n : β), dist (β(u n)) x =|x -β(u n)| Ξ΅: β Ξ΅_pos: Ξ΅ >0 R_pos: 0<ββ1/ Ξ΅ββ+1
h
(ββ1/ Ξ΅ββ+1)β»ΒΉ< Ξ΅
x: β A:= fun n => {q ||x -βq|<1/ (βn +1)}: β β Set β non_empty: β (n : β), (A n).Nonempty u:= fun n =>β―.some: β β β dst: β (n : β), dist (β(u n)) x =|x -β(u n)| Ξ΅: β Ξ΅_pos: Ξ΅ >0 R_pos: 0<ββ1/ Ξ΅ββ+1
h
Ξ΅β»ΒΉ<ββ1/ Ξ΅ββ+1
Goals accomplished!π
x: β A:= fun n => {q ||x -βq|<1/ (βn +1)}: β β Set β non_empty: β (n : β), (A n).Nonempty u:= fun n =>β―.some: β β β dst: β (n : β), dist (β(u n)) x =|x -β(u n)| Ξ΅: β Ξ΅_pos: Ξ΅ >0 R_pos: 0<ββ1/ Ξ΅ββ+1
h
1/ Ξ΅ <ββ1/ Ξ΅ββ+1
x: β A:= fun n => {q ||x -βq|<1/ (βn +1)}: β β Set β non_empty: β (n : β), (A n).Nonempty u:= fun n =>β―.some: β β β dst: β (n : β), dist (β(u n)) x =|x -β(u n)| Ξ΅: β Ξ΅_pos: Ξ΅ >0
β N, 1/ (βN +1) < Ξ΅
Goals accomplished!π
Goals accomplished!π
x: β
β u, Tendsto (fun n =>β(u n)) atTop (π x)
x: β A:= fun n => {q ||x -βq|<1/ (βn +1)}: β β Set β non_empty: β (n : β), (A n).Nonempty u:= fun n =>β―.some: β β β dst: β (n : β), dist (β(u n)) x =|x -β(u n)| Ξ΅: β Ξ΅_pos: Ξ΅ >0 N: β hn: 1/ (βN +1) < Ξ΅
h
β n > N, |x -β(u n)|< Ξ΅
x: β
β u, Tendsto (fun n =>β(u n)) atTop (π x)
x: β A:= fun n => {q ||x -βq|<1/ (βn +1)}: β β Set β non_empty: β (n : β), (A n).Nonempty u:= fun n =>β―.some: β β β dst: β (n : β), dist (β(u n)) x =|x -β(u n)| Ξ΅: β Ξ΅_pos: Ξ΅ >0 N: β hn: 1/ (βN +1) < Ξ΅ n: β N_ltn: n > N
h
|x -β(u n)|< Ξ΅
x: β
β u, Tendsto (fun n =>β(u n)) atTop (π x)
Goals accomplished!π
/--Let A be a family of disjoint, non-empty, open sets of β. Then A is countable. (Example 9 p.4)-/example (A : NNReal β Set β) (h_nonempty : β t, Set.Nonempty (A t)) (h_open : β t, IsOpen (A t)) (h_disjoint : β t1 t2, t1 β t2 β Disjoint (A t1) (A t2)) : countable {A t | t : NNReal} :=
Goals accomplished!π
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2)
countable {x |β t, A t = x}
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β
countable {x |β t, A t = x}
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2)
countable {x |β t, A t = x}
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β
countable {x |β t, A t = x}
Goals accomplished!π
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β
β (t : NNReal), (q_A_t t).Nonempty
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β
β (t : NNReal), (q_A_t t).Nonempty
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β
β (t : NNReal), (q_A_t t).Nonempty
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β t: NNReal
(q_A_t t).Nonempty
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β
β (t : NNReal), (q_A_t t).Nonempty
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β t: NNReal x: β hx: x β A t
intro
(q_A_t t).Nonempty
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β
β (t : NNReal), (q_A_t t).Nonempty
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β t: NNReal x: β hx: x β A t h_open: IsOpen (A t)
intro
(q_A_t t).Nonempty
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β
β (t : NNReal), (q_A_t t).Nonempty
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β t: NNReal x: β hx: x β A t h_open: IsOpen (A t)
intro
(q_A_t t).Nonempty
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β t: NNReal x: β hx: x β A t h_open: β x β A t, β Ξ΅ >0, Metric.ball x Ξ΅ β A t
intro
(q_A_t t).Nonempty
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β t: NNReal x: β hx: x β A t h_open: β x β A t, β Ξ΅ >0, Metric.ball x Ξ΅ β A t
intro
(q_A_t t).Nonempty
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β t: NNReal x: β hx: x β A t h_open: β x β A t, β Ξ΅ >0, Metric.ball x Ξ΅ β A t
intro
(q_A_t t).Nonempty
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β
β (t : NNReal), (q_A_t t).Nonempty
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β t: NNReal x: β hx: x β A t h_open: β x β A t, β Ξ΅ >0, Metric.ball x Ξ΅ β A t Ξ΅: β hΞ΅: Ξ΅ >0 ball_in_At: Metric.ball x Ξ΅ β A t
intro.intro.intro
(q_A_t t).Nonempty
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β
β (t : NNReal), (q_A_t t).Nonempty
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β t: NNReal x: β hx: x β A t h_open: β x β A t, β Ξ΅ >0, Metric.ball x Ξ΅ β A t Ξ΅: β hΞ΅: Ξ΅ >0 ball_in_At: Metric.ball x Ξ΅ β A t
intro.intro.intro
(q_A_t t).Nonempty
Goals accomplished!π
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β t: NNReal x: β hx: x β A t h_open: β x β A t, β Ξ΅ >0, Metric.ball x Ξ΅ β A t Ξ΅: β hΞ΅: Ξ΅ >0 ball_in_At: Metric.ball x Ξ΅ β A t q: β hql: x <βq hqr: βq < x + Ξ΅
intro.intro.intro.intro.intro
(q_A_t t).Nonempty
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β
β (t : NNReal), (q_A_t t).Nonempty
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β t: NNReal x: β hx: x β A t h_open: β x β A t, β Ξ΅ >0, Metric.ball x Ξ΅ β A t Ξ΅: β hΞ΅: Ξ΅ >0 ball_in_At: Metric.ball x Ξ΅ β A t q: β hql: x <βq hqr: βq < x + Ξ΅
intro.intro.intro.intro.intro
(q_A_t t).Nonempty
Goals accomplished!π
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β t: NNReal x: β hx: x β A t h_open: β x β A t, β Ξ΅ >0, Metric.ball x Ξ΅ β A t Ξ΅: β hΞ΅: Ξ΅ >0 ball_in_At: Metric.ball x Ξ΅ β A t q: β hql: x <βq hqr: βq < x + Ξ΅
intro.intro.intro.intro.intro
(q_A_t t).Nonempty
Goals accomplished!π
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β
β (t : NNReal), (q_A_t t).Nonempty
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β t: NNReal x: β hx: x β A t h_open: β x β A t, β Ξ΅ >0, Metric.ball x Ξ΅ β A t Ξ΅: β hΞ΅: Ξ΅ >0 ball_in_At: Metric.ball x Ξ΅ β A t q: β hql: x <βq hqr: βq < x + Ξ΅ q_dist: βq - x < Ξ΅
intro.intro.intro.intro.intro
(q_A_t t).Nonempty
Goals accomplished!π
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β t: NNReal x: β hx: x β A t h_open: β x β A t, β Ξ΅ >0, Metric.ball x Ξ΅ β A t Ξ΅: β hΞ΅: Ξ΅ >0 ball_in_At: Metric.ball x Ξ΅ β A t q: β hql: x <βq hqr: βq < x + Ξ΅ q_dist: βq - x < Ξ΅ pos_abs: βq - x =|βq - x|
intro.intro.intro.intro.intro
(q_A_t t).Nonempty
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β
β (t : NNReal), (q_A_t t).Nonempty
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β t: NNReal x: β hx: x β A t h_open: β x β A t, β Ξ΅ >0, Metric.ball x Ξ΅ β A t Ξ΅: β hΞ΅: Ξ΅ >0 ball_in_At: Metric.ball x Ξ΅ β A t q: β hql: x <βq hqr: βq < x + Ξ΅ q_dist: βq - x < Ξ΅ pos_abs: βq - x =|βq - x|
intro.intro.intro.intro.intro
(q_A_t t).Nonempty
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β t: NNReal x: β hx: x β A t h_open: β x β A t, β Ξ΅ >0, Metric.ball x Ξ΅ β A t Ξ΅: β hΞ΅: Ξ΅ >0 ball_in_At: Metric.ball x Ξ΅ β A t q: β hql: x <βq hqr: βq < x + Ξ΅ q_dist: |βq - x|< Ξ΅ pos_abs: βq - x =|βq - x|
intro.intro.intro.intro.intro
(q_A_t t).Nonempty
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β t: NNReal x: β hx: x β A t h_open: β x β A t, β Ξ΅ >0, Metric.ball x Ξ΅ β A t Ξ΅: β hΞ΅: Ξ΅ >0 ball_in_At: Metric.ball x Ξ΅ β A t q: β hql: x <βq hqr: βq < x + Ξ΅ q_dist: βq - x < Ξ΅ pos_abs: βq - x =|βq - x|
intro.intro.intro.intro.intro
(q_A_t t).Nonempty
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β t: NNReal x: β hx: x β A t h_open: β x β A t, β Ξ΅ >0, Metric.ball x Ξ΅ β A t Ξ΅: β hΞ΅: Ξ΅ >0 ball_in_At: Metric.ball x Ξ΅ β A t q: β hql: x <βq hqr: βq < x + Ξ΅ q_dist: |βq - x|< Ξ΅ pos_abs: βq - x =|βq - x|
intro.intro.intro.intro.intro
(q_A_t t).Nonempty
Goals accomplished!π
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β t: NNReal x: β hx: x β A t h_open: β x β A t, β Ξ΅ >0, Metric.ball x Ξ΅ β A t Ξ΅: β hΞ΅: Ξ΅ >0 ball_in_At: Metric.ball x Ξ΅ β A t q: β hql: x <βq hqr: βq < x + Ξ΅ q_dist: dist (βq) x < Ξ΅ pos_abs: βq - x =|βq - x|
intro.intro.intro.intro.intro
(q_A_t t).Nonempty
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β t: NNReal x: β hx: x β A t h_open: β x β A t, β Ξ΅ >0, Metric.ball x Ξ΅ β A t Ξ΅: β hΞ΅: Ξ΅ >0 ball_in_At: Metric.ball x Ξ΅ β A t q: β hql: x <βq hqr: βq < x + Ξ΅ q_dist: βq - x < Ξ΅ pos_abs: βq - x =|βq - x|
intro.intro.intro.intro.intro
(q_A_t t).Nonempty
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β t: NNReal x: β hx: x β A t h_open: β x β A t, β Ξ΅ >0, Metric.ball x Ξ΅ β A t Ξ΅: β hΞ΅: Ξ΅ >0 ball_in_At: Metric.ball x Ξ΅ β A t q: β hql: x <βq hqr: βq < x + Ξ΅ q_dist: βq β Metric.ball x Ξ΅ pos_abs: βq - x =|βq - x|
intro.intro.intro.intro.intro
(q_A_t t).Nonempty
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β t: NNReal x: β hx: x β A t h_open: β x β A t, β Ξ΅ >0, Metric.ball x Ξ΅ β A t Ξ΅: β hΞ΅: Ξ΅ >0 ball_in_At: Metric.ball x Ξ΅ β A t q: β hql: x <βq hqr: βq < x + Ξ΅ q_dist: βq β Metric.ball x Ξ΅ pos_abs: βq - x =|βq - x|
intro.intro.intro.intro.intro
(q_A_t t).Nonempty
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β t: NNReal x: β hx: x β A t h_open: β x β A t, β Ξ΅ >0, Metric.ball x Ξ΅ β A t Ξ΅: β hΞ΅: Ξ΅ >0 ball_in_At: Metric.ball x Ξ΅ β A t q: β hql: x <βq hqr: βq < x + Ξ΅ q_dist: βq β Metric.ball x Ξ΅ pos_abs: βq - x =|βq - x|
intro.intro.intro.intro.intro
(q_A_t t).Nonempty
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β
β (t : NNReal), (q_A_t t).Nonempty
Goals accomplished!π
Goals accomplished!π
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2)
countable {x |β t, A t = x}
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β)
countable {x |β t, A t = x}
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2)
countable {x |β t, A t = x}
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β)
countable {x |β t, A t = x}
Goals accomplished!π
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β)
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β)
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β)
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) q: β h: β t, q β q_A_t t
(q_A q).Nonempty
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β)
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) q: β t: NNReal hq: q β q_A_t t
intro
(q_A q).Nonempty
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β)
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) q: β t: NNReal hq: q β q_A_t t
h
A t = A t β§βq β A t
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β)
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) q: β t: NNReal hq: q β q_A_t t
h
βq β A t
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β)
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2)
countable {x |β t, A t = x}
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β
countable {x |β t, A t = x}
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2)
countable {x |β t, A t = x}
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β
countable {x |β t, A t = x}
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2)
countable {x |β t, A t = x}
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β
countable {x |β t, A t = x}
Goals accomplished!π
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β
SurjOn f univ {x |β t, A t = x}
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β
SurjOn f univ {x |β t, A t = x}
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β
SurjOn f univ {x |β t, A t = x}
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At
At β f '' univ
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β
SurjOn f univ {x |β t, A t = x}
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At
At β f '' univ
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At
A t β f '' univ
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At
A t β f '' univ
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β
SurjOn f univ {x |β t, A t = x}
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t
intro
A t β f '' univ
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β
SurjOn f univ {x |β t, A t = x}
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t
h
q β univ β§ f q = A t
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β
SurjOn f univ {x |β t, A t = x}
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t
h
f q = A t
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β
SurjOn f univ {x |β t, A t = x}
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t
h
f q = A t
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t
h
f q = A t
Goals accomplished!π
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t
h
(if h : β t, q β q_A_t t then Ο q h else A 0) = A t
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β
SurjOn f univ {x |β t, A t = x}
[Meta.Tactic.simp.rewrite] dif_pos:1000, if h : β t, q β q_A_t t then Ο q h else A 0==> Ο q hβ
[Meta.Tactic.simp.rewrite] dif_neg:1000, if h : β t, q β q_A_t t then Ο q h else A 0==> A 0
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t hβ: β t, q β q_A_t t
h.isTrue
Ο q hβ= A t
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t hβ: Β¬β t, q β q_A_t t
A 0= A t
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β
SurjOn f univ {x |β t, A t = x}
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t hβ: β t, q β q_A_t t
h.isTrue
Ο q hβ= A t
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t hβ: Β¬β t, q β q_A_t t
A 0= A t
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t h_if: β t, q β q_A_t t
Ο q h_if = A t
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t h_if: β t, q β q_A_t t
Ο q h_if = A t
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t h_if: β t, q β q_A_t t rfl_Ο: Ο q h_if β q_A q
Ο q h_if = A t
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t h_if: β t, q β q_A_t t
Ο q h_if = A t
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t h_if: β t, q β q_A_t t t2: NNReal h_eq_t2: A t2 = Ο q h_if hq2: βq β A t2
intro.intro
Ο q h_if = A t
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t h_if: β t, q β q_A_t t
Ο q h_if = A t
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t h_if: β t, q β q_A_t t t2: NNReal h_eq_t2: A t2 = Ο q h_if hq2: βq β A t2
intro.intro
Ο q h_if = A t
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t h_if: β t, q β q_A_t t t2: NNReal h_eq_t2: A t2 = Ο q h_if hq2: βq β A t2
intro.intro
A t2 = A t
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t h_if: β t, q β q_A_t t t2: NNReal h_eq_t2: A t2 = Ο q h_if hq2: βq β A t2
intro.intro
A t2 = A t
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t h_if: β t, q β q_A_t t
Ο q h_if = A t
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t h_if: β t, q β q_A_t t t2: NNReal h_eq_t2: A t2 = Ο q h_if hq2: βq β A t2
intro.intro
A t2 = A t
Goals accomplished!π
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t h_if: β t, q β q_A_t t t2: NNReal h_eq_t2: A t2 = Ο q h_if hq2: βq β A t2
A t = A t2
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t h_if: β t, q β q_A_t t t2: NNReal h_eq_t2: A t2 = Ο q h_if hq2: βq β A t2
A t = A t2
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t h_if: β t, q β q_A_t t t2: NNReal h_eq_t2: A t2 = Ο q h_if hq2: βq β A t2
A t = A t2
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t h_if: β t, q β q_A_t t t2: NNReal h_eq_t2: A t2 = Ο q h_if hq2: βq β A t2 h_neg: Β¬A t = A t2
False
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t h_if: β t, q β q_A_t t t2: NNReal h_eq_t2: A t2 = Ο q h_if hq2: βq β A t2 h_neg: Β¬A t = A t2
False
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t h_if: β t, q β q_A_t t t2: NNReal h_eq_t2: A t2 = Ο q h_if hq2: βq β A t2
A t = A t2
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t h_if: β t, q β q_A_t t t2: NNReal h_eq_t2: A t2 = Ο q h_if hq2: βq β A t2 h_neg: A t β A t2
False
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t h_if: β t, q β q_A_t t t2: NNReal h_eq_t2: A t2 = Ο q h_if hq2: βq β A t2
A t = A t2
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t h_if: β t, q β q_A_t t t2: NNReal h_eq_t2: A t2 = Ο q h_if hq2: βq β A t2 h_neg: A t β A t2 t_neq: t β t2
False
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t h_if: β t, q β q_A_t t t2: NNReal h_eq_t2: A t2 = Ο q h_if hq2: βq β A t2
A t = A t2
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t h_if: β t, q β q_A_t t t2: NNReal h_eq_t2: A t2 = Ο q h_if hq2: βq β A t2 h_neg: A t β A t2 t_neq: t β t2 disjoint: Disjoint (A t) (A t2)
False
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t h_if: β t, q β q_A_t t t2: NNReal h_eq_t2: A t2 = Ο q h_if hq2: βq β A t2
A t = A t2
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t h_if: β t, q β q_A_t t t2: NNReal h_eq_t2: A t2 = Ο q h_if hq2: βq β A t2 h_neg: A t β A t2 t_neq: t β t2 disjoint: Disjoint (A t) (A t2) q_not_in: βq β A t2
False
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t h_if: β t, q β q_A_t t t2: NNReal h_eq_t2: A t2 = Ο q h_if hq2: βq β A t2
A t = A t2
Goals accomplished!π
Goals accomplished!π
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t h_if: β t, q β q_A_t t
Ο q h_if = A t
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t h_if: β t, q β q_A_t t t2: NNReal h_eq_t2: A t2 = Ο q h_if hq2: βq β A t2 At_eq_At2: A t = A t2
intro.intro
A t2 = A t
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t h_if: β t, q β q_A_t t t2: NNReal h_eq_t2: A t2 = Ο q h_if hq2: βq β A t2 At_eq_At2: A t = A t2
intro.intro
A t2 = A t2
Goals accomplished!π
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β
SurjOn f univ {x |β t, A t = x}
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t hβ: Β¬β t, q β q_A_t t
h.isFalse
A 0= A t
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t h_if: β (t : NNReal), q β q_A_t t
A 0= A t
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t h_if: Β¬β t, q β q_A_t t
A 0= A t
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t h_if: q β q_A_t t
A 0= A t
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2) q_A_t:= fun t => {q |βq β A t}: NNReal β Set β nonempty_q_A_t: β (t : NNReal), (q_A_t t).Nonempty q_A:= fun q => {x |β t, A t = x β§βq β A t}: β β Set (Set β) nonempty_q_A: β (q : β), (β t, q β q_A_t t) β (q_A q).Nonempty Ο:= fun q hq =>β―.some: (q : β) β (β t, q β q_A_t t) β Set β f:= fun q =>if h : β t, q β q_A_t t then Ο q h else A 0: β β Set β At: Set β t: NNReal h: A t = At q: β hq: q β q_A_t t h_if: Β¬β t, q β q_A_t t
A 0= A t
Goals accomplished!π
Goals accomplished!π
A: NNReal β Set β h_nonempty: β (t : NNReal), (A t).Nonempty h_open: β (t : NNReal), IsOpen (A t) h_disjoint: β (t1 t2 : NNReal), t1 β t2 β Disjoint (A t1) (A t2)