leanprover-community/mathlib3

Pull Requests Commits

feat(data/fin/tuple/monotone): new file (#14483)

urkud committed 3 years ago

741f4deb

feat(set_theory/cardinal/cofinality): basic lemmas on limit cardinals (#14439)

vihdzp committed 3 years ago

f65b160d

chore(data/pi/lex): turn `pi.lex.linear_order` into an instance (#14389)

urkud committed 3 years ago

d136cd55

feat(measure_theory/integral/interval_integral): integrability of nonnegative derivatives on open intervals (#14147)

khwilson committed 3 years ago

97492975

refactor(topology/vector_bundle): split file (#14535)

fpvandoorn committed 3 years ago

93fb5345

feat(analysis/special_functions/exp): a lemma about `exp (f x) =O[l] const _ _` (#14524)

urkud committed 3 years ago

3103a89b

feat(tactic/set): fix a bug (#14488)

alexjbest committed 3 years ago

19b57866

feat(analysis/asymptotics/asymptotics): generalize `is_*.inv_rev` (#14486)

urkud committed 3 years ago

a869df9e

refactor(data/fin/basic): reformulate `fin.strict_mono_iff_lt_succ` (#14482)

urkud committed 3 years ago

8a6a7933

refactor(order/directed): use `(≥)` instead of `swap (≤)` (#14474)

urkud committed 3 years ago

cab5a456

feat(measure_theory/measure/measure_space): there exists a ball of positive measure (#14449)

urkud committed 3 years ago

b5973ba9

chore(data/finsupp/basic): make arguments explicit (#14551)

eric-wieser committed 3 years ago

cfcc3a1b

feat(algebra/{lie/subalgebra,module/submodule/pointwise}): submodules and lie subalgebras form canonically ordered additive monoids under addition (#14529)

eric-wieser committed 3 years ago

b9492402

feat(set_theory/cardinal/cofinality): `ω` is a strong limit cardinal (#14436)

vihdzp committed 3 years ago

83c1cd8a

feat(set_theory/cardinal/cofinality): limit cardinal is at least `ω` (#14432)

vihdzp committed 3 years ago

0746194f

move(set_theory/{schroeder_bernstein → cardinal/schroeder_bernstein}): move file (#14426)

vihdzp committed 3 years ago

15726ee0

feat(data/list/nodup): Add `list.nodup_iff` (#14371)

user7230724 committed 3 years ago

1f196cb2

doc(set_theory/ordinal/natural_ops): mention alternate names (#14546)

vihdzp committed 3 years ago

aa7d90bc

chore(order/bounded_order): move `order_dual` instances up, use them to golf lemmas (#14544)

urkud committed 3 years ago

8ef2c02c

refactor(topology): move code around (#14525)

urkud committed 3 years ago

50024528

perf(measure_theory/probability_mass_function/monad): speed up proof (#14519)

vihdzp committed 3 years ago

66b618d2

feat(data/int/basic): Units are either equal or negatives of each other (#14517)

tb65536 committed 3 years ago

3f26dfe2

feat(data/int/basic): Forward direction of `is_unit_iff_nat_abs_eq` (#14516)

tb65536 committed 3 years ago

b332507c

feat(analysis/special_functions): lemmas about filter `map`/`comap` (#14513)

urkud committed 3 years ago

2a9be5b5

feat(order/boolean_algebra, set/basic): some compl lemmas (#14508)

apnelson1 committed 3 years ago

0e943b15

feat(set_theory/ordinal/arithmetic): `has_exists_add_of_le` instance for `ordinal` (#14499)

vihdzp committed 3 years ago

27c4241b

feat(order/bounds): Bounds on `set.image2` (#14306)

YaelDillies committed 3 years ago

7c57af94

feat(order/conditionally_complete_lattice,data/real/nnreal): add 2 lemmas (#14545)

urkud committed 3 years ago

85fffda8

feat(data/multiset/basic): add some lemmas (#14421)

Ruben-VandeVelde committed 3 years ago

72ac40e9

chore(set_theory/surreal/basic): golf (#14168)

vihdzp committed 3 years ago

a418945a

Newer Older