urkud
Follow
urkud
Follow
Popular repositories
1,705 contributions in the last year
Less
More
Activity overview
Contributed to
leanprover-community/mathlib,
urkud/bib,
leanprover-community/lean
and 1 other
repository
Contribution activity
January 2022
Created 44 commits in 1 repository
Created a pull request in leanprover-community/mathlib that received 6 comments
Opened 42 other pull requests in 1 repository
leanprover-community/mathlib
6
open
36
closed
- feat(analysis/convex/integral): strict Jensen's inequality
-
feat(*): lemmas about
disjointonsets andfilters -
feat(measure_theory/measure): drop more
measurable_setargs - [Merged by Bors] - chore(order/bounded_order): golf
-
[Merged by Bors] - feat(measure_theory): drop some
measurable_setassumptions -
[Merged by Bors] - feat(measure_theory): generalize
null_of_locally_nulltoouter_measure, add versions -
[Merged by Bors] - feat(topology/separation): add
t1_space_tfae - [Merged by Bors] - feat(topology/metric_space): more lemmas about disjoint balls
-
[Merged by Bors] - feat(measure_theory): generalize some lemmas to
outer_measure -
[Merged by Bors] - feat(measure_theory/measure): define
ae_disjoint -
[Merged by Bors] - feat(measure_theory/measure): add lemmas, drop
measurable_setassumptions -
[Merged by Bors] - feat(*): add a few lemmas about
function.extend - [Merged by Bors] - feat(data/equiv/encodable): add a few lemmas
- [Merged by Bors] - chore(data/list/big_operators): rename vars, reorder lemmas
- [Merged by Bors] - feat(analysis/calculus/dslope): define dslope
-
[Merged by Bors] - chore(analysis/calculus/{deriv,mean_value}): use
slope -
[Merged by Bors] - feat(analysis/complex/cauchy_integral): review docs, add versions without
off_countable - [Merged by Bors] - chore(order/lattice_intervals): review
-
[Merged by Bors] - feat(order,data/set/intervals): lemmas about
is_bot/is_top - [Merged by Bors] - doc(data/pfun): fix a typo
-
[Merged by Bors] - feat(analysis/asymptotics/asymptotics): add
is_bounded_under.is_O_const -
[Merged by Bors] - refactor(topology/connected): drop
local attribute [instance] connected_component_setoid -
[Merged by Bors] - feat(analysis/calculus/{f,}deriv): add some
ifflemmas -
[Merged by Bors] - refactor(linear_algebra/affine_space): move def of
slopeto a new file - [Merged by Bors] - feat(topology): a few simple lemmas
- Some pull requests not shown.
Reviewed 21 pull requests in 2 repositories
leanprover-community/mathlib
20 pull requests
- [Merged by Bors] - feat(measure_theory/measure/measure_space): better definition of to_measurable
- doc(polynomial/eval): why map_ring_hom can't replace map
- feat(set_theory/ordinal_arithmetic): The derivative of addition
- [Merged by Bors] - feat(data/set): two simple lemmas
-
[Merged by Bors] - feat(measure_theory/measure): define
ae_disjoint - feat(topology/algebra/mul_action2): quotient by a properly discontinuous group action is t2
- refactor(order/well_founded_set): golf, review API
- [Merged by Bors] - fix(order/complete_lattice): fix diamond in sup vs max and min vs inf
- [Merged by Bors] - feat(order/well_founded_set): Antichains in a partial well order are finite
- [Merged by Bors] - refactor(data/set/prod): add notation class for set-like product
- [Merged by Bors] - feat(measure_theory/integral): weaker assumptions on Ioi integrability
- [Merged by Bors] - feat(analysis/inner_product_space/basic): criterion for summability
- [Merged by Bors] - feat(data/polynomial/{erase_lead + denoms_clearable}): strengthen a lemma
- feat(analysis/special_functions/{log, pow}): add log_base
-
feat(topology/continuous/algebra) : giving
C(α, R)ahas_continuous_smulstructure - [Merged by Bors] - feat(topology/*): Gluing topological spaces
-
[Merged by Bors] - chore(analysis/inner_product_space/basic): extract common
variables - [Merged by Bors] - feat(algebra/ring/basic): Introduce non-unital, non-associative rings
- [Merged by Bors] - feat(algebra/associated): add lemmas to split #9345
-
[Merged by Bors] - refactor(logic/small, *): Infer
f : α → βwhen followed by a simple condition onf