More problems #4
Conversation
|
Many thanks! I will take a look at these today before my 8pm livestream. |
There was a problem hiding this comment.
This PR is not really a PR, it is a plan! (Actually I think his is quite a good use of draft PRs). It has many distinct changes. There are some additions to level 1 which need discussion. There are some results about addition proved in a world about filters, and this needs some discussion. And then there are some results about infinite intersections which deviate from Lean's standard notation for these things, and this option is definitely not on the table :-) There are lots of independent things which need to be discussed. Will try and collect my thoughts.
| @@ -38,7 +38,15 @@ because it's precisely the *definition* of `𝓟 A`. | |||
| -/ | |||
| TheoremDoc MyGame.mem_principal as "mem_principal" in "Filter" | |||
|
|
|||
| NewTheorem MyGame.mem_principal | |||
| lemma univ_mem_principal {A : Set 𝓧} : A ∈ 𝓟 A := by rw [mem_principal] | |||
There was a problem hiding this comment.
I think my policy for lemma naming in this game is that, like tactics, everything should match mathlib. 𝓟 is notation for Filter.principal in the Filter scope, and you can loogle for this lemma and then copy the mathlib name.
Furthermore, this should surely be its own level, rather than something given to the user.
There was a problem hiding this comment.
Ah, I didn’t know loogle exists. I’ll take a look at that.
| @@ -16,6 +16,31 @@ namespace MyGame | |||
|
|
|||
| open Filter | |||
|
|
|||
| -- Might put these in earlier exercises? | |||
| lemma le_self_add {a b : ℕ} : a ≤ a + b := by | |||
There was a problem hiding this comment.
I think we don't need these as exercises. These are easy if you have access to the NNG framework but we don't have access to any of that documentation here. We just give access to them as axioms using the mathlib implementation. I'm not entirely sure we need them though: I am not sure we need natural addition in filter world.
There was a problem hiding this comment.
In principle, for this particular problem and neighbourhood filter, we just need the fact that the intersection of two open sets is again open, but having another world to explain why
| Introduction "In this level, we'll see the definition and some properties of the infinite intersection of a filter." | ||
|
|
||
| def inter (f : Filter α) : Set α := { a | ∀ s ∈ f, a ∈ s } | ||
| notation "∩'" => inter |
There was a problem hiding this comment.
We need to use mathlib's notation here, not make up our own.
|
|
||
|
|
||
| example {S T : Set 𝓧} (hST : 𝓟 S = 𝓟 T) : S = T := by | ||
| have h : ∩' (𝓟 T) = T := inter_principal_eq_base |
There was a problem hiding this comment.
We would need to have a have level in tactic world for this to be a valid approach.
This added quite a few problems but they are not well-documented yet and unorganised. Notably, we have
Feedbacks are welcome.