leanprover-community/mathlib3

Pull Requests Commits

Putting changes back to ordinal.basic, since there are more files under the tide now

sterraf committed 2 years ago

b7089a4a

Definition of initial ordinals; eliminating superfluous lemma; restoring ordinal.basic

sterraf committed 2 years ago

1f89414b

Update src/set_theory/cardinal/ordinal.lean

sterraf committed 2 years ago

Verified cd3b013e

Docstring, indentation

sterraf committed 3 years ago

6b083065

Moving to constructions dir

sterraf committed 3 years ago

5f831da5

Suggested edits.

sterraf committed 3 years ago

3b3e2aef

Apply suggestions from code review

sterraf committed 3 years ago

Verified 6b7993c2

Update src/measure_theory/borel_hierarchy.lean

sterraf committed 3 years ago

Verified 1d651067

Apply suggestions from code review

sterraf committed 3 years ago

Verified 68b14e9d

More docstrings & minor code edits

sterraf committed 3 years ago

fdfd1ef8

Delete section on cardinality of sigma-algebras for later.

sterraf committed 3 years ago

e41dfa7a

Update src/measure_theory/borel_hierarchy.lean

sterraf committed 3 years ago

Verified 687247d7

sterraf committed 3 years ago

3571ea23

Changes to documentation suggested by S. Gouëzel.

sterraf committed 3 years ago

28b7e8bd

Update src/set_theory/cardinal/ordinal.lean

sterraf committed 3 years ago

Verified b5e9bf61

Update src/measure_theory/borel_hierarchy.lean

sterraf committed 3 years ago

Verified 94589184

Update src/measure_theory/borel_hierarchy.lean

sterraf committed 3 years ago

Verified a064690e

fix line width and copyright statement

sterraf committed 3 years ago

77a211df

feat(measure_theory): define Borel hiearchy and reprove cardinality bound on σ-algebras

sterraf committed 3 years ago

9f796b5a

sterraf committed 3 years ago

ef43db14

feat(set_theory): define `ω₁` and prove new lemma on cardinality of `Union`

sterraf committed 3 years ago

fc09f947

chore(number_theory/divisors): golf (#17954)

urkud committed 3 years ago

c2337ec8

feat(combinatorics/quiver/*): More edge reversal constructions (#17665)

bottine committed 3 years ago

706d88f2

feat(measure_theory/integral/layercake): Add versions of layercake formula with strict inequality. (#17920)

kkytola committed 3 years ago

11bb0c91

feat(measure_theory/measure/measure_space): A `measurable_equiv` is `quasi_measure_preserving` (#17774)

YaelDillies committed 3 years ago

2c5df64a

feat(dynamics/ergodic/ergodic): expand ergodic map API for finite measures (#17864)

ocfnash committed 3 years ago

809e920e

refactor(measure_theory/group/fundamental_domain): Use `pairwise` (#17928)

YaelDillies committed 3 years ago

d5ca915d

chore(order/monovary): Move (#17946)

YaelDillies committed 3 years ago

b3f25363

feat(measure_theory/covering) weaken sigma_compact_space to second_countable_topology (#17960)

sgouezel committed 3 years ago

d012cd09

chore(data/finset/lattice): Protect ambiguous lemmas (#17938)

YaelDillies committed 3 years ago

302eab4f

Older