Commits leanprover-community/mathlib

feat(data/real/{nnreal,ennreal}, topology/instances/ennreal): add of_real_(sum/prod/tsum) for nnreal and ennreal (#5896)

RemyDegenne committed 5 years ago

531bcd8d

feat(data/finset/basic): card_subtype simp lemma (#5894)

pechersky committed 5 years ago

8c732b2c

feat(analysis/{analytic,calculus}): an analytic function is strictly differentiable (#5878)

urkud committed 5 years ago

547d67fc

chore(data/finset): Rename bind to bUnion (#5813)

kmill committed 5 years ago

44fd23d1

chore(scripts): update nolints.txt (#5892)

leanprover-community-bot committed 5 years ago

01a7cde6

feat(data/fintype/basic): add lemmas about finsets and cardinality (#5886)

agusakov committed 5 years ago

5491c592

chore(algebra/group_with_zero): correct instance name (#5885)

eric-wieser committed 5 years ago

7f25aa76

feat(data/set/finite): add to_finset lemma (#5883)

agusakov committed 5 years ago

3a16e9f8

feat(data/set/finite): add lemma about to_finset of complement of set (#5881)

agusakov committed 5 years ago

ba876475

chore(algebra/pi_tensor_product): Replace use of classical with decidable_eq (#5880)

eric-wieser committed 5 years ago

7188d806

feat(analysis/normed_space/inner_product): double orthogonal complement is closure (#5876)

hrmacbeth committed 5 years ago

1dfa81a1

chore(algebra): a few more `@[mono]` tags (#5874)

urkud committed 5 years ago

ee750e33

feat(measure_theory/{measure_space, borel_space, integration}): prove ae_measurable for various limits (#5849)

RemyDegenne committed 5 years ago

6d806348

chore(archive/sensitivity): split long lines (#5882)

urkud committed 5 years ago

d6d4435e

feat(order/atoms): define (co)atomic, (co)atomistic lattices (#5588)

awainverse committed 5 years ago

9117ad71

chore(scripts): update nolints.txt (#5873)

leanprover-community-bot committed 5 years ago

87202fe9

feat(analysis/specific_limits): formula for `∑' n, n * r ^ n` (#5835)

urkud committed 5 years ago

507c7ffc

chore(linear_algebra/multilinear): Relax ring to semiring, add_comm_group to add_comm_monoid (#5870)

eric-wieser committed 5 years ago

5222db01

feat(order/complete_well_founded, data/finset/lattice): introduce compact elements of a complete lattice and characterize compact lattices as those with all elements compact (#5825)

cemulate committed 5 years ago

fbabe427

feat(data/nat/basic): add decidable_exists_lt deciding existence of a natural below a bound satisfying a predicate (#5864)

alexjbest committed 5 years ago

5db7a188

feat(measure_theory/lp_space): define Lp, subtype of ae_eq_fun with finite norm (#5853)

RemyDegenne committed 5 years ago

49c53d4f

feat(topology/subset_properties): a locally compact space with second countable topology is sigma compact (#5689)

fpvandoorn committed 5 years ago

aa744dba

feat(analysis/analytic/composition): filling small holes in existing API (#5822)

sgouezel committed 5 years ago

f414fcaa

chore(scripts): update nolints.txt (#5865)

leanprover-community-bot committed 5 years ago

160d243d

feat(algebra/pointwise): a lemma about pointwise addition/multiplication of bdd_above sets (#5859)

alexjbest committed 5 years ago

8da574f5

refactor(analysis/analytic/composition): extend definition, extract a lemma from a proof (#5850)

sgouezel committed 5 years ago

3a136f81

chore(set_theory/ordinal): use rel_iso notation in ordinal (#5857)

alexjbest committed 5 years ago

74760f22

feat(order/rel_iso): generalise several lemmas to assume only has_le not preorder (#5858)

alexjbest committed 5 years ago

013b902d

chore(scripts): update nolints.txt (#5856)

leanprover-community-bot committed 5 years ago

b0e874e0

docs(undergrad.yaml): update with #5724 and #5788 (#5855)

hrmacbeth committed 5 years ago

04972f69