{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":749221182,"defaultBranch":"master","name":"mathlib4","ownerLogin":"FormalMathematicsLab","currentUserCanPush":false,"isFork":true,"isEmpty":false,"createdAt":"2024-01-27T23:13:05.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/157014821?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1706397191.644518","currentOid":""},"activityList":{"items":[{"before":"46974e92276c335b41277addf83df55f8c080702","after":"89415b3911b02465645869fe39936a0d05d0f5fe","ref":"refs/heads/master","pushedAt":"2024-02-25T20:33:40.000Z","pushType":"push","commitsCount":7,"pusher":{"login":"pitmonticone","name":"Pietro Monticone","path":"/pitmonticone","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/38562595?s=80&v=4"},"commit":{"message":"feat: `small_iUnion` and `small_sUnion` (#10921)\n\nAlso moves the other results about `Small` on sets to their own file.","shortMessageHtmlLink":"feat: <code>small_iUnion</code> and <code>small_sUnion</code> (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2152255546\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover-community/mathlib4/issues/10921\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover-community/mathlib4/pull/10921/hovercard\" href=\"https://github.com/leanprover-community/mathlib4/pull/10921\">leanprover-community#10921</a>)"}},{"before":"6af752e0797f7a8ca9ef05fb5e7378d627cd264f","after":"46974e92276c335b41277addf83df55f8c080702","ref":"refs/heads/master","pushedAt":"2024-02-25T13:36:37.000Z","pushType":"push","commitsCount":10,"pusher":{"login":"pitmonticone","name":"Pietro Monticone","path":"/pitmonticone","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/38562595?s=80&v=4"},"commit":{"message":"chore: bump aesop; update syntax (#10955)\n\n\n\nCo-authored-by: Scott Morrison <scott.morrison@gmail.com>","shortMessageHtmlLink":"chore: bump aesop; update syntax (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2152716178\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover-community/mathlib4/issues/10955\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover-community/mathlib4/pull/10955/hovercard\" href=\"https://github.com/leanprover-community/mathlib4/pull/10955\">leanprover-community#10955</a>)"}},{"before":"d3dbfd96d551bb78ae75db33df18a386bda9b81b","after":"6af752e0797f7a8ca9ef05fb5e7378d627cd264f","ref":"refs/heads/master","pushedAt":"2024-02-24T20:42:52.000Z","pushType":"push","commitsCount":4,"pusher":{"login":"pitmonticone","name":"Pietro Monticone","path":"/pitmonticone","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/38562595?s=80&v=4"},"commit":{"message":"chore: classify `added lemma` porting notes (#10926)","shortMessageHtmlLink":"chore: classify <code>added lemma</code> porting notes (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2152401182\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover-community/mathlib4/issues/10926\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover-community/mathlib4/pull/10926/hovercard\" href=\"https://github.com/leanprover-community/mathlib4/pull/10926\">leanprover-community#10926</a>)"}},{"before":"f5e69ecacbe618607a2f1607d93d6938964d245c","after":"d3dbfd96d551bb78ae75db33df18a386bda9b81b","ref":"refs/heads/master","pushedAt":"2024-02-24T16:26:51.000Z","pushType":"push","commitsCount":26,"pusher":{"login":"pitmonticone","name":"Pietro Monticone","path":"/pitmonticone","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/38562595?s=80&v=4"},"commit":{"message":"chore(MeasureTheory): move Measure/OuterMeasure to `OuterMeasure/Basic` (#10916)\n\nI'm going to generalize some constructions\r\nfrom measures to outer measures and this file is already too large.","shortMessageHtmlLink":"chore(MeasureTheory): move Measure/OuterMeasure to `OuterMeasure/Basi…"}},{"before":"09b44c176e0eaf2a3cbf11272dca8cbe8dfcda29","after":"f5e69ecacbe618607a2f1607d93d6938964d245c","ref":"refs/heads/master","pushedAt":"2024-02-23T15:37:46.000Z","pushType":"push","commitsCount":705,"pusher":{"login":"pitmonticone","name":"Pietro Monticone","path":"/pitmonticone","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/38562595?s=80&v=4"},"commit":{"message":"feat: add `measurableSet_tendsto_nhds` (#10146)\n\nAdd `measurableSet_tendsto`: the set of points for which a measurable sequence of functions converges to a given filter is measurable.\r\n\r\n\n\nCo-authored-by: Rémy Degenne <remydegenne@gmail.com>","shortMessageHtmlLink":"feat: add <code>measurableSet_tendsto_nhds</code> (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2110294974\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover-community/mathlib4/issues/10146\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover-community/mathlib4/pull/10146/hovercard\" href=\"https://github.com/leanprover-community/mathlib4/pull/10146\">leanprover-community#10146</a>)"}}],"hasNextPage":false,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEBL0iyQA","startCursor":null,"endCursor":null}},"title":"Activity · FormalMathematicsLab/mathlib4"}