rubin-lean4

ee3cdfe13b :up_arrow: Upgrade mathlib main Shad Amethyst 2024-01-04 19:59:49 +0100
def2e9c37c 💄 added Emilie to authors laurent-lost-commits Laurent Bartholdi 2024-01-07 22:23:50 +0100
3753948ac8 💥 tried to add rubin Laurent Bartholdi 2024-01-07 22:22:06 +0100
253c33035d 🎉 Finished the proof of rubin's theorem Shad Amethyst 2024-01-01 17:00:19 +0100
8737257190 🎉 Construct the equivariant homeomorphism to the rubin space Shad Amethyst 2024-01-01 01:07:26 +0100
7d92d98b60 🎉 Finally reached the homeomorph stage! Shad Amethyst 2023-12-30 22:42:24 +0100
7c5ce7e631 ✨ Working equiv for RubinSpace Shad Amethyst 2023-12-30 16:54:11 +0100
6b2f21fec8 ✨ Fix all sorries Shad Amethyst 2023-12-29 23:28:20 +0100
6a2f4960d7 ✨ Construct ultrafilters in the topolical space and rubinfilters from one another Shad Amethyst 2023-12-29 16:19:46 +0100
5fb9162950 ✨ Prove that UltrafilterInBasis is a sufficient condition for convergence Shad Amethyst 2023-12-28 12:42:36 +0100
431a2931d7 ✨ Implement UltrafilterInBasis.map_basis Shad Amethyst 2023-12-27 22:36:22 +0100
e84ff177bd ✨ Start working on Filter.InBasis Shad Amethyst 2023-12-27 12:49:26 +0100
7b4307d76c ✨ Split apart the implications of theorem 3.5 to be able to use ultraprefilters Shad Amethyst 2023-12-26 11:19:33 +0100
ec9587c7e9 🔥 Draft out the end of the proof Shad Amethyst 2023-12-22 02:32:12 +0100
65e1ab7fc8 📝 Refactor RegularSupportBasis Shad Amethyst 2023-12-21 23:28:48 +0100
60111656b8 ✨ Replace ContinuousMulAction with ContinuousConstSMul Shad Amethyst 2023-12-21 20:16:42 +0100
a87dc079d6 💩 Messy draft code to work towards the end of the proof Shad Amethyst 2023-12-21 19:18:55 +0100
50b4b49932 ✨ Fully prove proposition 3.5 Shad Amethyst 2023-12-17 18:39:08 +0100
24dd2c4f0a 🔥 New notation for RigidStabilizer and prove first lemma for proposition 3.5 Shad Amethyst 2023-12-17 17:01:03 +0100
522f345f34 ✨ Implement SMul on filters, prove compactness of smulImage and that orbit is a subset of support Shad Amethyst 2023-12-17 15:56:34 +0100
23d0821290 ✨ Almost complete proof of proposition 3.5 Shad Amethyst 2023-12-17 01:08:28 +0100
55d674e96a ✨ Implement RigidStabilizerBasis and AlgebraicCentralizerBasis Shad Amethyst 2023-12-09 00:51:54 +0100
5d81de14d4 🚚 Move RegularSupportBasis to its own file Shad Amethyst 2023-12-08 14:41:31 +0100
9e6258bf5c 🚚 Rename AssociatedPoset to RegularSupportBasis Shad Amethyst 2023-12-08 14:37:12 +0100
cfb341daeb Added rubin Laurent Bartholdi 2023-12-03 18:15:10 +0100
52b5b5523b 📝 Add installation instructions and push to github Shad Amethyst 2023-12-04 00:37:06 +0100
7afc87d0f9 ⬆️ Upgrade mathlib and lean version to latest Shad Amethyst 2023-12-02 21:39:59 +0100
69ad593f4b ✨ Prove proposition 3.2 Shad Amethyst 2023-12-02 15:10:29 +0100
a09187c7fa ✨ Start proving proposition 3.2 Shad Amethyst 2023-12-02 13:43:06 +0100
29fc8990a8 ✨ Prove the two-way monotonicity of rigid stabilizers in group homeomorphisms Shad Amethyst 2023-12-01 21:35:23 +0100
3b0b8a8a65 ✨ Define group action from HomeoGroup to AssociatedPoset Shad Amethyst 2023-12-01 16:21:26 +0100
652e1a0773 🚚 Move a bunch of definitions around, making Topology importable from more files Shad Amethyst 2023-12-01 13:21:23 +0100
18912139ec Rename smulImage_subset to smulImage_mono Shad Amethyst 2023-12-01 12:35:01 +0100
03cec8913a ✨ Start working on homeomorphic groups Shad Amethyst 2023-11-30 23:37:12 +0100
d5cd873cf6 ✨ Implement remark 2.3 Shad Amethyst 2023-11-30 01:25:04 +0100
7a8184548b 🚚 Move proofs of Rubin's theorem to Rubin.lean Shad Amethyst 2023-11-29 21:01:02 +0100
6ce7127efe 🎨 Small renames for consistency Shad Amethyst 2023-11-29 20:47:29 +0100
4b4a719d40 ✨ Working proof of proposition 2.1 Shad Amethyst 2023-11-27 18:28:34 +0100
6815874923 A quick fix to prop 2.1, just to test laurentbartholdi 2023-11-27 15:47:59 +0100
fc12acb37b ✨ Implement most of proposition 2.1 Shad Amethyst 2023-11-27 03:17:40 +0100
4d8a4d0f1a ✨ Transition over RegularSupport Shad Amethyst 2023-11-26 02:42:35 +0100
9df983f476 ✨ Clean up algebraic disjointness Shad Amethyst 2023-11-25 13:17:29 +0100
43784b1210 ✨ Translate and clean up up to remark 1.2 Shad Amethyst 2023-11-25 03:13:16 +0100
cd9ad02e1d ✨ Prove disjoint_nbhd_fin Shad Amethyst 2023-11-24 15:58:12 +0100
d96318acc8 ✨ Translate proposition 1.1.1 to lean4 Shad Amethyst 2023-11-24 00:36:26 +0100
171caae2d3 ✨ Move out toplogical actions and faithful actions Shad Amethyst 2023-11-23 13:21:15 +0100
adc7194774 🚚 Start moving more theorems in different files Shad Amethyst 2023-11-21 01:31:12 +0100
5fcca86b58 🚚 Move tactic to Rubin/Tactic.lean, wrap everything in a namespace Shad Amethyst 2023-11-20 23:33:23 +0100
049434fcd8 ✨ Implement the group_action tactic Shad Amethyst 2023-11-20 22:05:52 +0100
76ad77cd09 ✨ No more compilation errors :) Shad Amethyst 2023-11-20 12:13:51 +0100
a8c3cd1aa1 Fix most issues with porting Shad Amethyst 2023-11-20 02:42:01 +0100
80349c3496 Remove namespace that conflicted with #aligns Shad Amethyst 2023-11-20 01:44:49 +0100
7806ecb35e ✨ Raw port through mathport Shad Amethyst 2023-11-20 01:27:43 +0100
6470249db0 ✨ Add lean3 version of rubin's wip proof Shad Amethyst 2023-11-20 00:33:37 +0100

Commit Graph Select branches Hide Pull Requests laurent-lost-commits main #1 Mono Color

Commit Graph

Select branches

Hide Pull Requests

laurent-lost-commits

main

#1