Zulip Chat Archive

Stream: Analysis I

Topics:

Ukrainian translation of Analysis I (1 message, latest: Feb 24 2026 at 07:06)
Restarting the effort and keeping up with the times (5 messages, latest: Feb 11 2026 at 06:33)
Chapter 5 epilogue: isomorphism with the Mathlib real number (32 messages, latest: Feb 02 2026 at 20:08)
Exercise 3.5.12 question (4 messages, latest: Dec 30 2025 at 20:39)
Teaching a class on Analysis I with Lean outside academia? (13 messages, latest: Nov 04 2025 at 06:52)
Exercise 6.1.10 mismatch (4 messages, latest: Nov 02 2025 at 06:06)
Using well-defined induction in Chapter 2 (1 message, latest: Oct 28 2025 at 04:41)
Definition of Sequence Add and Mul instances in 6.1 (4 messages, latest: Oct 24 2025 at 06:40)
Play-testing progress (4 messages, latest: Oct 22 2025 at 04:26)
Appendix B.1 - using exist statement in def (12 messages, latest: Oct 09 2025 at 13:40)
Proof fragility in Ch3.6 (4 messages, latest: Sep 27 2025 at 20:28)
Moving to grind (9 messages, latest: Sep 26 2025 at 22:15)
Confused by the hint in 3.6.12 (20 messages, latest: Sep 17 2025 at 14:34)
Extensionality on Sequence (4 messages, latest: Sep 17 2025 at 11:30)
Understanding the use of injection in Ch2.1 (15 messages, latest: Sep 15 2025 at 19:29)
ch5.5 - two definitions of |.| (35 messages, latest: Sep 13 2025 at 15:22)
Transforming inequality in Reals to Q (or vice versa) (11 messages, latest: Sep 12 2025 at 06:40)
Some additional theorems for proving ex5.5.4 (6 messages, latest: Sep 11 2025 at 21:31)
Issue with verso pages not rendering (5 messages, latest: Sep 10 2025 at 08:22)
Alternative proof for 5.3 eq_lim (4 messages, latest: Sep 03 2025 at 19:56)
Zero in 3.6.14 cardinality exercises (8 messages, latest: Sep 02 2025 at 16:53)
[ch5.1] real number inequalities with concrete numbers (5 messages, latest: Sep 01 2025 at 06:42)
Missing exercise 5.1.2 (5 messages, latest: Aug 31 2025 at 00:09)
Chapter 4 done and question about 4.4.3 (2 messages, latest: Aug 28 2025 at 19:41)
exercise 4.3.4 needs extra hypothesis (6 messages, latest: Aug 25 2025 at 02:58)
Repositories/forks with exercise solutions (17 messages, latest: Aug 24 2025 at 23:00)
ch4.2 - mysterious error when building inst CommRing Rat (13 messages, latest: Aug 24 2025 at 22:59)
Doc-gen no longer building (38 messages, latest: Aug 21 2025 at 10:24)
exercise 3.5.12 - how to do induction through an equivalence (4 messages, latest: Aug 19 2025 at 19:03)
Should Exercise 3.5.12 have a second part? (4 messages, latest: Aug 13 2025 at 20:43)
How to prove this equation(x>0, Odd n, (-x)^(1/n)=-x^(1/n))? (8 messages, latest: Aug 12 2025 at 23:18)
Which exercise does iProd_equiv_tuples correspond to? (2 messages, latest: Aug 12 2025 at 02:50)
blog post on my experience of learning lean so far (1 message, latest: Aug 11 2025 at 02:30)
Getting stuck with a HEq goal in 3.5.2 (23 messages, latest: Aug 10 2025 at 22:23)
ch 4.1 - why is natCast automatically distributed over + (7 messages, latest: Aug 08 2025 at 01:07)
Chapter 3 done - ex 3.6.12 is harder than I expected (9 messages, latest: Aug 06 2025 at 03:41)
Does 3.5.10 (singleton_iProd_equiv) have a simpler solution? (28 messages, latest: Aug 05 2025 at 10:08)
Struggling to understand SetTheory.Set.tuple/iProd (3 messages, latest: Aug 04 2025 at 19:46)
Chapter 2: Nat.trichotomous may not be powerful enough (7 messages, latest: Aug 04 2025 at 19:21)
Using axiom of choice in chapters 2 and 3 and .choose (6 messages, latest: Aug 03 2025 at 22:34)
hitting the dreaded motive rw error in 3.6.10 (11 messages, latest: Aug 01 2025 at 15:32)
Regression with simps? (15 messages, latest: Jul 31 2025 at 23:45)
Missing axioms for various injections into Object? (11 messages, latest: Jul 31 2025 at 03:34)
Deciding on membership in Chapter 3 (1 message, latest: Jul 29 2025 at 07:08)
[Exercise 3.4.7] How to work with Props that have let_fun (27 messages, latest: Jul 29 2025 at 04:29)
✔ Is Exercise 3.4.6 (ii) missing? (22 messages, latest: Jul 27 2025 at 02:45)
Is there a way to hide internals of a definition in Lean? (4 messages, latest: Jul 24 2025 at 11:27)
Sets as predicates vs ZFC (7 messages, latest: Jul 22 2025 at 23:49)
Chapter 3.5 done - example 3.5.9 slowdown (3 messages, latest: Jul 22 2025 at 19:00)
exercise 3.5.12 rewrite with nat literal fails again (27 messages, latest: Jul 19 2025 at 21:48)
a true proof assistant wow moment (6 messages, latest: Jul 17 2025 at 18:57)
Math question about 5.3.10 (4 messages, latest: Jul 17 2025 at 18:54)
View build logs without sorry? (4 messages, latest: Jul 17 2025 at 07:12)
Formalization complete (5 messages, latest: Jul 17 2025 at 05:40)
✔ Should Ch3.5 OrderedPair.toObject be def too (4 messages, latest: Jul 17 2025 at 05:04)
✔ Ch 3.5 example - failing to rewrite (13 messages, latest: Jul 17 2025 at 01:13)
Ch 3.5 OrderedPair eval APIs (2 messages, latest: Jul 16 2025 at 08:25)
✔ Example 3.5.11 - switching types of implicit arguments (4 messages, latest: Jul 16 2025 at 03:10)
✔ Where can I buy latest edition as a PDF? (3 messages, latest: Jul 15 2025 at 20:51)
Is there a more Lean-y approach to coercions? (5 messages, latest: Jul 15 2025 at 18:58)
Tao's Analysis Ch3.3 (45 messages, latest: Jul 14 2025 at 19:25)
✔ exercise 3.5.2 - how to extract a type equality from terms (27 messages, latest: Jul 14 2025 at 04:19)
✔ Exercise 3.2.3: Only one direction? (6 messages, latest: Jul 10 2025 at 00:39)
✔ rechecking the project from the CLI (3 messages, latest: Jul 09 2025 at 14:26)
✔ Chapter 3.2 not_mem_self exercise can't infer SetTheory (11 messages, latest: Jul 09 2025 at 00:13)
Best practices with powerful tactics (6 messages, latest: Jul 08 2025 at 16:33)
Naming conventions (9 messages, latest: Jul 08 2025 at 02:19)
Relationship between literals and OfNat instances (47 messages, latest: Jul 07 2025 at 19:59)
Lean companion to "Analysis I" - discussion (257 messages, latest: Jul 07 2025 at 08:22)
✔ Can this proof related to Set replacement be shorter? (64 messages, latest: Jul 07 2025 at 04:19)
Help with solving Tao's Analysis Chapter 2 epilogue problem (29 messages, latest: Jul 07 2025 at 02:37)
✔ Why doesn't rw match my pattern? (7 messages, latest: Jul 07 2025 at 02:36)
Why is equivalence of type, zero, and succ sufficient here? (12 messages, latest: Jul 07 2025 at 02:36)
✔ help with Tao's Analysis Ch3.1 exercise (26 messages, latest: Jul 07 2025 at 02:35)
channel events (1 message, latest: Jul 06 2025 at 21:20)

Last updated: Feb 28 2026 at 14:05 UTC