Project idea: Cantor set

Stream: LFTCM 2024

[Emilie Uthaiwat]

Hello everyone,

This is the stream for the project on the Cantor set.

[Suraj Krishna M S]

I would like to join this project

[JB Stiegler]

Hello ! I'm interested, but i'm a total beginner. I can also go to the group project about proper grouo actions if we are too many in here

[Isabelle Dubois]

I'm in. Isabelle

[Alina Yan]

I'm interested

[Alina Yan]

Isabelle Dubois said:

I'm in. Isabelle

My first thought was that you want to implement it in Isabelle theorem prover :joy:

[JB Stiegler]

Hello, i checked and the Hausdorff distance is already implemented in Lean (and the even stronger version of Gromov): https://www.moogle.ai/search/raw?q=haussdorf%20distance
It might be usefull for defining the Cantor set, because it is an attractor for this distance. But maybe it's not realistic, i'm new to Lean

[Filippo A. E. Nuccio]

This is a third equivalent definition, and it would also be nice. We might meet after all talks in the library and discuss where to go....

[Lorenzo Zanichelli]

What kind of equivalent definitions are we interested in? Is it feasible to prove that the Cantor set is the only compact second countable zero-dimensional perfect topological space, up to homeomorphism?

[Lorenzo Zanichelli]

(deleted)

[JB Stiegler]

Apparently Filippo has a pdf with a proof of that, which we could implement

[JB Stiegler]

This is the interesting fact that is useful

[Anatole Dedecker]

If you do so I think it will make your life much easier (and make the theorem much more useful) to prove that the only space such that [...] is $\{0, 1\}^\mathbb{N}$ and then show that triadic Cantor satisfies [...]

[JB Stiegler]

yeah but then it doesn't make much sense in here to show that 1/4 is in the set... but then again, the interesting fact is the theorem

[Lorenzo Zanichelli]

But what is our starting definition for the Cantor Set? The triadic one? Or is the Cantor Set not even defined at all in Lean

[Anatole Dedecker]

I don't think we have anything in the library. Let's talk about this during the coffee break maybe?

[Jana Göken]

Sure :)

[JB Stiegler]

I checked and I think that there is no definition of cantor set in lean

[Alina Yan]

image.png

[Filippo A. E. Nuccio]

The best thing to do is to create a fork and to push there; is this OK?

[Filippo A. E. Nuccio]

When @Emilie Uthaiwat was pushing, she got an error "cannot push to master branch: create a fork instead"? Click yes, and then share the url of this fork with the others who can clone/push.

[Emilie Uthaiwat]

https://github.com/EmilieUthaiwat/LFTCM2024/tree/master/LFTCM2024

[Emilie Uthaiwat]

This is the link to the file on which we can work.

[Suraj Krishna M S]

Please post your GitHub usernames here so that Emilie can add you as collaborators to the project

[Riccardo Brasca]

If you need push rights to the main repo just ask me, no problem

[Tomáš Jakl]

I was using why my intuition is all wrong when trying to prove some of the lemmas, turns out that our pre_Cantor_set functino is wrong. There should be no (n-1) in the definition.

[Emilie Uthaiwat]

Absolutely. I'm sorry about that.

[Tomáš Jakl]

No problem ;-)

[Tomáš Jakl]

I'll fix it

[Tomáš Jakl]

So I have a working proof that zero is in the Cantor set

[Tomáš Jakl]

I used the rewriting tricks from Isabelle's file

[Suraj Krishna M S]

I pushed a file to the project, with a proof of zero_in_Cantor. I don't know how my proof differs from that of @Tomáš Jakl. Would be happy if someone with better Lean proficiency helps me understand :)

[Suraj Krishna M S]

Tomáš Jakl said:

I was using why my intuition is all wrong when trying to prove some of the lemmas, turns out that our pre_Cantor_set functino is wrong. There should be no (n-1) in the definition.

Thanks for discovering this!

[Filippo A. E. Nuccio]

Can I check what the git status of the project is? Are we all aligned using @Emilie Uthaiwat 's fork? Is it updated with everybody's results?

[Suraj Krishna M S]

I was able to push mine.

[Lorenzo Zanichelli]

So, now that we a working definition and working push rights, I believe we are finally ready to work on the following goals, split into teams: I propose, for now:
Team 1 works on the alternative definition found on Wikipedia and on proving they're the same
Team 2 works on proving that 1/4 is in the Cantor set
Team 3 starts working on proving the basic properties topological of the Cantor set.

[Lorenzo Zanichelli]

A proof for Team 2 should be inductive, as the one provided by John here: https://math.stackexchange.com/questions/289803/1-4-is-in-the-cantor-set

[Filippo A. E. Nuccio]

I think that the following is slightly easier for 2.:

To say that $1/4\in C$ means that for all $n$ there is a $0\le k\le 3^{n-1}$ such that either $1/4 \in [3k/3^n,(3k+1)/3n]$ or $1/4\in [(3k+2)/3^n,3(k+1)/3^n]$. In turns this means that we need to find an $a\in \mathbb{N}$ such that

1. $a≤(3^n)/4≤a+1$
2. $a\not\equiv 1\pmod{3}$.

Now, since $n$ is fixed we can look at $3^n$, that would be either $1\pmod{4}$ or $3\pmod{4}$. The first condition then becomes, respectively,
1a. $a≤1/4+m≤a+1$ (where $3^n=1+4m$); or
1b. $a≤3/4+m≤a+1$ (where $3^n=3+4m$).

In both cases, I suggest to take $a=m$, that clearly satisfies both 1a and 1b, so 1 is satisfied. We are left to prove that $m\not\equiv 1\pmod{3}$ (remember that $m$ is the number such that $3^n=x+4m$ where $x\in\{1,3\}$). Reducing the above equation modulo $3$ it becomes either $0\equiv 1+m\pmod{3}$ or $0\equiv 0+m\pmod{3}$, and in both cases $m$ is not $1$ modulo 3.

But of course also the "analytic" argument above is fine, do the one that you prefer!

[Isabelle Dubois]

Filippo A. E. Nuccio said:

Can I check what the git status of the project is? Are we all aligned using Emilie Uthaiwat 's fork? Is it updated with everybody's results?

I would need help to manage all this push/pull stuff in VSCode. I'm not able to do resolve my problems by myself.

[Filippo A. E. Nuccio]

Isabelle Dubois said:

Filippo A. E. Nuccio said:

Can I check what the git status of the project is? Are we all aligned using Emilie Uthaiwat 's fork? Is it updated with everybody's results?

I would need help to manage all this push/pull stuff in VSCode. I'm not able to do resolve my problems by myself.

I will come right after the talk.

[Isabelle Dubois]

Filippo A. E. Nuccio said:

Isabelle Dubois said:

Filippo A. E. Nuccio said:

Can I check what the git status of the project is? Are we all aligned using Emilie Uthaiwat 's fork? Is it updated with everybody's results?

I would need help to manage all this push/pull stuff in VSCode. I'm not able to do resolve my problems by myself.

I will come right after the talk.

thanks!

[Lorenzo Zanichelli]

shall we meet somewhere soon? Maybe in the same place as yesterday in the library?

[JB Stiegler]

yes ! when everybody finish there teas, we could meet in the library like yesterday ?

[Emilie Uthaiwat]

Filippo told me that we can now go to the library to work on the project

[Lorenzo Zanichelli]

Just a reminder that while our files are named Cantor_Set, the actual Cantor set is named Cantor_set... pay attention!

[Lorenzo Zanichelli]

Major change necessary for my team! The definition of Cantor space must be adjusted: we need TL, TR in the definition to be homeomorphisms, otherwise proving the topological properties will be impossible.

[Suraj Krishna M S]

Lorenzo Zanichelli said:

Major change necessary for my team! The definition of Cantor space must be adjusted: we need TL, TR in the definition to be homeomorphisms, otherwise proving the topological properties will be impossible.

Can these properties be proved for the two functions without modifying the definition? Changing the definition might make it more cumbersome as we don't use any topology there.

[Riccardo Brasca]

Being an isomorphism is not a property that exists in mathlib (I think). The property is bundled.. but leaveI the experienced users in your team explain what this means :sweat_smile:

[Riccardo Brasca]

In particular this means that the required change is only Lean related, mathematically nothing happens

[Riccardo Brasca]

You can also prove that your function satisfies docs#IsClosedMap, but maybe at some point you will need it is an homeomorphism, and it is probably better to have it as homeomorphism from the beginning

[Anatole Dedecker]

Can I discuss a bit about this with you ? I haven't followed everything closely but I want to make sure you're not making your life harder

[Artur Szafarczyk]

Lorenzo Zanichelli said:

Major change necessary for my team! The definition of Cantor space must be adjusted: we need TL, TR in the definition to be homeomorphisms, otherwise proving the topological properties will be impossible.

Aren't they homeomorphisms?

[Filippo A. E. Nuccio]

Lorenzo Zanichelli said:

Major change necessary for my team! The definition of Cantor space must be adjusted: we need TL, TR in the definition to be homeomorphisms, otherwise proving the topological properties will be impossible.

At any rate to define that something is a homeo you need that it is a function first of all :smile: We discuss this after the talk.

[Lorenzo Zanichelli]

BTW, all current goals of Group 3 are now properly stated in Lorenzo.Zanichelli.lean, and I've started working on some of them if you want to take a look :wink:

[Sam van G]

Artur Szafarczyk said:

Lorenzo Zanichelli said:

Major change necessary for my team! The definition of Cantor space must be adjusted: we need TL, TR in the definition to be homeomorphisms, otherwise proving the topological properties will be impossible.

Aren't they homeomorphisms?

Yes, they are, and you could use some of the techniques Jireh is explaining to try to find something in the library that lets you to prove this to Lean!

[JB Stiegler]

The 1/4 is in Cantor is done

[Alina Yan]

Let's all meet tomorrow at 10:30 in the same room downstairs at the library. So that we update each other on our progress, synchronize (e.g. maybe merge some files) and agree on how to continue

[Filippo A. E. Nuccio]

Here is something that fits in the margin
report5.pdf

[Lorenzo Zanichelli]

Filippo A. E. Nuccio said:

Here is something that fits in the margin
report5.pdf

the proof for stage 4) starts on page 9.
page 6 might be of interest to prove that Cantor is perfect.

[Lorenzo Zanichelli]

tomorrow we're going to the sea

[Artur Szafarczyk]

Is the proof of 1/4 in Cantor finished in the end?

[Artur Szafarczyk]

Ah, ok I see now.

[Tomáš Jakl]

Where did you guys go? I can't find you in the library.

[Jana Göken]

@Artur Szafarczyk heading to library now

[Artur Szafarczyk]

I'm coming

[Artur Szafarczyk]

I pushed

[Jana Göken]

thaaaaanks :pray::pray::pray::pray::pray:

[Isabelle Dubois]

For Team 1 - in your definition there's a lack of parenthesis I think : ((3*k+1)/3^n) instead of (3*k+1/3^n)

[Suraj Krishna M S]

Isabelle Dubois said:

For Team 1 - in your definition there's a lack of parenthesis I think : ((3*k+1)/3^n) instead of (3*k+1/3^n)

Indeed. Thanks. Will fix it.

[Jana Göken]

/poll Do you want to participate in a the Rocq practice session or rather work on the Cantor project?
I want to work on Cantor project
I want to practice some Rocq

[Jana Göken]

Hey! I am not really interested in Rocq right now and would like to continue on the project. I thought maybe someone else would like to join?

[Jana Göken]

also I would love to meet up again today with the whole group at some point. Tomorrow we should present the project, so it would be a goo idea to discuss the further progress and also how we present

[Isabelle Dubois]

Jana Göken said:

Hey! I am not really interested in Rocq right now and would like to continue on the project. I thought maybe someone else would like to join?

I want to practice Rocq but feel free to work on the project without me, especially team 3.

[JB Stiegler]

Filippo A. E. Nuccio said:

Here is something that fits in the margin
report5.pdf

I have a slight remark on this. The lemma 2.7 states:
"Any compact perfect totally disconnected subset E of the real line is homeomorphic to the Cantor set C".
And the proof uses the fact that we are in \R (with inf and sup). This is okay to prove that the Z_p are homeomorphic (as we see them in \R). But i thought that the lemma is more general (= not needing to be a subset of \R). I'll look for a proof of that, if it's easy i'll post it here.

[JB Stiegler]

Okay so i found this paper that explains it quite well (btw the lemma 2.7 is a Brouwer's theorem): https://arxiv.org/pdf/1210.1008.pdf
To prove the most general statement, they first prove the ordered version. I'll try to write a skeleton of the proof from the first paper then : )

[Jana Göken]

I suggest we meet at 17:30 in the usual room then :)

[JB Stiegler]

i'm on the first floor of the library if someone want to work with me before the conference resumes

[Filippo A. E. Nuccio]

Oliver Nash is currently given a tutorial on Topology and Filters: I believe it can be very useful for everbody in the project!

[Floris van Doorn]

I noticed that we can characterize what it means to be totally disconnected in the reals, which will be useful for this project.

import Mathlib.Analysis.Calculus.ContDiff.Basic -- an arbitrarily large import

open Set

lemma ordConnected_inter_Icc_of_subset {X : Type*} [LinearOrder X] {x y : X} {s : Set X}
    (h : Ioo x y ⊆ s) : OrdConnected (s ∩ Icc x y) := by
  simp_rw [ordConnected_iff]
  intros u hu v hv _huv w hw
  have h2w : w ∈ Icc x y := ⟨hu.2.1.trans hw.1, hw.2.trans hv.2.2⟩
  refine ⟨?_, h2w⟩
  by_cases hwu : w = u
  · subst w; exact hu.1
  by_cases hwv : w = v
  · subst w; exact hv.1
  refine h ⟨h2w.1.lt_of_ne ?_, h2w.2.lt_of_ne ?_⟩
  · rintro rfl; exact hwu <| hu.2.1.antisymm hw.1
  · rintro rfl; exact hwv <| hw.2.antisymm hv.2.2

lemma exists_nmem_between_of_not_OrdConnected {X : Type*} [LinearOrder X] {x y : X} {s : Set X}
    (h : ¬ OrdConnected (s ∩ Icc x y)) : ∃ z ∉ s, z ∈ Ioo x y := by
  have := mt ordConnected_inter_Icc_of_subset h
  simp_rw [subset_def, not_forall, exists_prop, and_comm (b := _ ∉ _)] at this
  exact this

lemma ordConnected_inter_Icc_iff {X : Type*} [LinearOrder X] {x y : X} {s : Set X}
    (hx : x ∈ s) (hy : y ∈ s) : OrdConnected (s ∩ Icc x y) ↔ Ioo x y ⊆ s := by
  refine ⟨fun h z hz ↦ ?_, ordConnected_inter_Icc_of_subset⟩
  simp_rw [ordConnected_iff] at h
  have hxy : x ≤ y := hz.1.trans hz.2 |>.le
  exact h x ⟨hx, le_rfl, hxy⟩ y ⟨hy, hxy, le_rfl⟩ hxy ⟨hz.1.le, hz.2.le⟩ |>.1

lemma not_ordConnected_inter_Icc_iff {X : Type*} [LinearOrder X] {x y : X} {s : Set X}
  (hx : x ∈ s) (hy : y ∈ s) : ¬ OrdConnected (s ∩ Icc x y) ↔ ∃ z ∉ s, z ∈ Ioo x y := by
  simp_rw [ordConnected_inter_Icc_iff hx hy, subset_def, not_forall, exists_prop, and_comm]

lemma isTotallyDisconnected_iff_le {X : Type*}
    [TopologicalSpace X] [ConditionallyCompleteLinearOrder X]
    [OrderTopology X] [DenselyOrdered X] {s : Set X} :
    IsTotallyDisconnected s ↔ ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∉ s, x < z ∧ z < y := by
  simp_rw [IsTotallyDisconnected, isPreconnected_iff_ordConnected, ← not_nontrivial_iff]
  refine ⟨fun h x hx y hy hxy ↦ ?_, fun h t hts ht ⟨x, hx, y, hy, hxy⟩ ↦ ?_⟩
  · simp_rw [← mem_Ioo, ← not_ordConnected_inter_Icc_iff hx hy]
    refine fun hs ↦ h _ (inter_subset_left _ _) hs ?_
    exact ⟨x, ⟨hx, le_rfl, hxy.le⟩, y, ⟨hy, hxy.le, le_rfl⟩, hxy.ne⟩
  · obtain hxy|hxy := hxy.lt_or_lt
    · obtain ⟨z, h1z, h2z⟩ := h x (hts hx) y (hts hy) hxy
      exact h1z <| hts <| ht.1 hx hy ⟨h2z.1.le, h2z.2.le⟩
    · obtain ⟨z, h1z, h2z⟩ := h y (hts hy) x (hts hx) hxy
      exact h1z <| hts <| ht.1 hy hx ⟨h2z.1.le, h2z.2.le⟩

[JB Stiegler]

wow, this is great, thanks !
I have a question for you: do you know if the theorem "an open of R is a countable union of open intervals" is in mathlib ? I couldn't find it...

[Floris van Doorn]

docs#Real.isTopologicalBasis_Ioo_rat together with docs#TopologicalSpace.IsTopologicalBasis.open_iff_eq_sUnion gives you that an open of R is a union of open intervals with rational endpoints.
Let me think how you get countability...

[Floris van Doorn]

I guess docs#TopologicalSpace.isOpen_sUnion_countable then gives you a countable subcollection.

[Floris van Doorn]

I found it using
@loogle IsOpen, Set.Countable

[Floris van Doorn]

@loogle IsOpen, Set.Countable

[loogle]

:search: TopologicalSpace.isOpen_sUnion_countable, TopologicalSpace.isOpen_iUnion_countable, and 14 more

[Jana Göken]

plan change: we meet in 10min

[JB Stiegler]

IMG_20240328_170119.jpg
The plan for team 1

[Filippo A. E. Nuccio]

@Alina Yan Are you somewhere, do you want to meet?

[Suraj Krishna M S]

Team 1 is still working, so we won't join for the meeting now

[Artur Szafarczyk]

I managed to push.

[Jana Göken]

Okay so I just tried and did a first PR :3 However "Lint Style" and "Check all files imported" failed. But I guess this is a good opportunity to get to know the process of a PR while we are still here and can ask experts . :blush:

[Suraj Krishna M S]

I get the following error when I open the Team 1 file: stderr:
info: [1499/1500] Building LFTCM2024.Cantor_Set.Cantor_Set
error: > LEAN_PATH=./.lake/packages/std/.lake/build/lib:./.lake/packages/Qq/.lake/build/lib:./.lake/packages/aesop/.lake/build/lib:./.lake/packages/proofwidgets/.lake/build/lib:./.lake/packages/Cli/.lake/build/lib:./.lake/packages/importGraph/.lake/build/lib:./.lake/packages/mathlib/.lake/build/lib:./.lake/build/lib DYLD_LIBRARY_PATH=./.lake/packages/std/.lake/build/lib:./.lake/packages/Qq/.lake/build/lib:./.lake/packages/aesop/.lake/build/lib:./.lake/packages/proofwidgets/.lake/build/lib:./.lake/packages/Cli/.lake/build/lib:./.lake/packages/importGraph/.lake/build/lib:./.lake/packages/mathlib/.lake/build/lib:./.lake/build/lib:/Users/suraj/.elan/toolchains/leanprover--lean4---v4.7.0-rc2/lib/lean:/Users/suraj/.elan/toolchains/leanprover--lean4---v4.7.0-rc2/lib:./.lake/build/lib /Users/suraj/.elan/toolchains/leanprover--lean4---v4.7.0-rc2/bin/lean ./././LFTCM2024/Cantor_Set/Cantor_Set.lean -R ././. -o ./.lake/build/lib/LFTCM2024/Cantor_Set/Cantor_Set.olean -i ./.lake/build/lib/LFTCM2024/Cantor_Set/Cantor_Set.ilean -c ./.lake/build/ir/LFTCM2024/Cantor_Set/Cantor_Set.c

Does anyone know what this means?

[Floris van Doorn]

Jana Göken said:

Okay so I just tried and did a first PR :3 However "Lint Style" and "Check all files imported" failed. But I guess this is a good opportunity to get to know the process of a PR while we are still here and can ask experts . :blush:

Congrats!
There are a bunch of style requirements for Mathlib files. You can read them here:
https://leanprover-community.github.io/contribute/style.html
I'm happy to help later.

[Jana Göken]

Thanks! Yeah that would be great! :D

[Suraj Krishna M S]

Jana Göken said:

Okay so I just tried and did a first PR :3 However "Lint Style" and "Check all files imported" failed. But I guess this is a good opportunity to get to know the process of a PR while we are still here and can ask experts . :blush:

Looks great!

[Riccardo Brasca]

You can write here a link to your PR, and someone will surely have a look (just write # 123456, without the space)

[Jana Göken]

Yes, I agree. Tom did a lot of golfing yesterday together with Floris!^^

[Jana Göken]

Sure! #11761

[Riccardo Brasca]

The style guide linked above explains how to solve most issues, it is essentially a matter of starting the file with a copyright header and to add a documentation to any def. Concerning the continuous integration / Check all files imported (push) error, it is enough to do

find Mathlib -name "*.lean" | env LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean

I have no idea why we don't do this automatically or at least suggest the solution :sweat_smile:

[Jana Göken]

Okay thanks!

[Tomáš Jakl]

Jana Göken said:

Okay so I just tried and did a first PR :3 However "Lint Style" and "Check all files imported" failed. But I guess this is a good opportunity to get to know the process of a PR while we are still here and can ask experts . :blush:

Can you please link the PR from Github here?

[Tomáš Jakl]

Suraj Krishna M S said:

I get the following error when I open the Team 1 file: stderr:
info: [1499/1500] Building LFTCM2024.Cantor_Set.Cantor_Set
error: > LEAN_PATH=./.lake/packages/std/.lake/build/lib:./.lake/packages/Qq/.lake/build/lib:./.lake/packages/aesop/.lake/build/lib:./.lake/packages/proofwidgets/.lake/build/lib:./.lake/packages/Cli/.lake/build/lib:. ....

Does anyone know what this means?

Are you still having this problem?

[Jana Göken]

Jana Göken schrieb:

Sure! #11761

It's this one ^^

[Tomáš Jakl]

A little warning, after including the content of all teams into the main file we were told by some of the Lean experts how to make the code leaner. One result of this is that we defined "Homeomorph_T_L" and "Homeomorph_T_R" by using certain combinators that give you that these are homeomorphisms for free. This caused minor breakage. Please ask here if it cases any big problems.

[Tomáš Jakl]

Jana Göken said:

Jana Göken schrieb:

Sure! #11761

It's this one ^^

Thanks!

This PR is from 3am! You really delivered on what I promised :smile:

[Jana Göken]

Riccardo Brasca schrieb:

The style guide linked above explains how to solve most issues, it is essentially a matter of starting the file with a copyright header and to add a documentation to any def. Concerning the continuous integration / Check all files imported (push) error, it is enough to do

find Mathlib -name "*.lean" | env LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean

If I try to put that line somewhere in the beginning of my file it always gives me error messages:
CantorSet.lean:12:0
unexpected identifier; expected command
CantorSet.lean:12:78
invalid 'import' command, it must be used in the beginning of the file

Do you have any idea why this is?

[Jana Göken]

Tomáš Jakl schrieb:

Jana Göken said:

Jana Göken schrieb:

Sure! #11761

It's this one ^^

Thanks!

This PR is from 3am! You really delivered on what I promised :smile:

Well I told you to push for a reason :grinning_face_with_smiling_eyes:

[Riccardo Brasca]

Jana Göken said:

Riccardo Brasca schrieb:

The style guide linked above explains how to solve most issues, it is essentially a matter of starting the file with a copyright header and to add a documentation to any def. Concerning the continuous integration / Check all files imported (push) error, it is enough to do

find Mathlib -name "*.lean" | env LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean

If I try to put that line somewhere in the beginning of my file it always gives me error messages:
CantorSet.lean:12:0
unexpected identifier; expected command
CantorSet.lean:12:78
invalid 'import' command, it must be used in the beginning of the file

Do you have any idea why this is?

Sorry, you have to type it in a terminal, not in a Lean file.

[Riccardo Brasca]

If you open the terminal inside VS Code it should already be in the right place. It modifies a file that you have to stage and commit as usual.

[Jana Göken]

ohhhh okay I will try

[Isabelle Dubois]

Jana Göken said:

ohhhh okay I will try

I guess you are trying to propose our file somewhere for Mathlib. Thanks for that and your work. I might add that I don't understand anything about the problems you encounter, and all the process to do it.

[Suraj Krishna M S]

Tomáš Jakl said:

Suraj Krishna M S said:

I get the following error when I open the Team 1 file: stderr:
info: [1499/1500] Building LFTCM2024.Cantor_Set.Cantor_Set
error: > LEAN_PATH=./.lake/packages/std/.lake/build/lib:./.lake/packages/Qq/.lake/build/lib:./.lake/packages/aesop/.lake/build/lib:./.lake/packages/proofwidgets/.lake/build/lib:./.lake/packages/Cli/.lake/build/lib:. ....

Does anyone know what this means?

Are you still having this problem?

Filippo helped me solve it: it happened because my file was importing the main Cantor set file and this one had errors. So some of the errors in the Cantor set file now appear below a #exit command so they don't actually compile.

Some of the problems were caused by someone copying our code to the Cantor set file. That has been fixed now.

[Filippo A. E. Nuccio]

If you are still struggling with it I am happy to help

[Artur Szafarczyk]

While on the train, I proved some small things in Is_TotallyDisconnected_Cantor_attempt2 in Jana's file.

[Jana Göken]

Isabelle Dubois schrieb:

Jana Göken said:

ohhhh okay I will try

I guess you are trying to propose our file somewhere for Mathlib. Thanks for that and your work. I might add that I don't understand anything about the problems you encounter, and all the process to do it.

Exactly^^ No problem

[Jana Göken]

Hey guys! I hope you all had some great easter days! :smiling_face: I wanted to thank you all for the great time and also for your work! I really enjoyed the collaboration on the cantor set project with you guys and I admire how everybody did their best, it was a great week!
Even during easter days, Tom has been working quite a lot on the PR, special thanks for that! I guess we will keep you updated about its status. :)

[Jana Göken]

Hey guys! Just wanted to keep you updated. The merge is complete now! :D Feel free to add some of your further theorems if you want ^_^

[Jireh Loreaux]

@Jana Göken This is my fault (because I suggested the text in the docstring), but Ruben Van de Velde pointed out after merging that the second function in preCantorSet is described wrong in the docstring (and hence also in the module documentation). If you fix it and ping me, I'll merge it quickly.

[Artur Szafarczyk]

Jana Göken said:

Hey guys! Just wanted to keep you updated. The merge is complete now! :D Feel free to add some of your further theorems if you want ^_^

Congrats to @Jana Göken and @Tomáš Jakl!
(and all the reviewers too!)

[Jireh Loreaux]

I didn't follow all the work you did in Luminy. Some nice follow-up could be to generalize to fat Cantor sets and compute the Lebesgue measure.

[Isabelle Dubois]

Jana Göken said:

Hey guys! Just wanted to keep you updated. The merge is complete now! :D Feel free to add some of your further theorems if you want ^_^

Thanks! I'm still working on the bijection between the Cantor set and triadic expansion of a real in the unit interval, and its topological consequences.
Where can we find what we have done, and how to proceed if we want to add new theorems?

[Filippo A. E. Nuccio]

@Jana Göken Do you want to answer this, especially concerning how you learned about adding new theorems?

[Tomáš Jakl]

@Isabelle Dubois I think you can freely ignore what we've pushed to the mathlib. Feel free to work in your own file, as before, and at the end I'll merge it into the main one once this is done.

[Isabelle Dubois]

Tomáš Jakl said:

Isabelle Dubois I think you can freely ignore what we've pushed to the mathlib. Feel free to work in your own file, as before, and at the end I'll merge it into the main one once this is done.

Ok, thanks!

[Jana Göken]

Isabelle Dubois schrieb:

Jana Göken said:

Hey guys! Just wanted to keep you updated. The merge is complete now! :D Feel free to add some of your further theorems if you want ^_^

Thanks! I'm still working on the bijection between the Cantor set and triadic expansion of a real in the unit interval, and its topological consequences.
Where can we find what we have done, and how to proceed if we want to add new theorems?

That's great to hear! What you could also do is clone the mathlib4 project. Then create a new branch. On that branch you can add work to the cantor set file. The advantage would be that you see if your code compiles in that file. Because we had to change some of our work. For example we deleted the homeomorphisms, meaning they dont have names anymore.
But feel free to do it either way! ^_^

[Filippo A. E. Nuccio]

Let me remind you of the existence of the tag lftcm24 for PR's coming from the conference.

[Isabelle Dubois]

Ok, I'll try to find out in Mathlib where to find the new files. I have to say I'm still not at ease with all the cloning and merging stuff.

[Filippo A. E. Nuccio]

Do not hesitate to ask for help!

[Filippo A. E. Nuccio]

This might help

[Tomáš Jakl]

But please do not get stuck with it. If you just want to have fun and do Lean, instead of figuring out how all this git+github+mathlib combo works then feel free to do so.