Louis Wasserman

icon indicating an email [email protected]

icon company @google icon location Mountain View, CA icon location I am the Kotlin lead on the Java and Kotlin Ecosystem team at Google, which organizes libraries, frameworks, and the language ecosystem as a whole.

Results 167 comments of Louis Wasserman

Riemann integration

That might actually be easier to prove by working directly with classical-Fin and constructing a new equivalence, rather than the preexisting product-Fin...

Non-denumerability of the continuum

I'm uncertain. I am mostly planning to go from Bishop's proof in Foundations of Constructive Analysis, and I don't see any choice principles in that proof yet; he accepts countable...

Non-denumerability of the continuum

I see now that it uses dependent choice, actually.

Simplifications for Theorem 11.2.12 {RD-cauchy-complete}

Was already working on it. Sent!

Maximum heap size reached on `category-theory.codensity-monads-on-precategories`

#1341 seems to be hitting this too.

Dependent sums and products of cardinals

I'm excited to see this work; I attempted once or twice to tackle the commutative semiring of cardinalities but didn't get very far.

Bolzano's theorem

Is this theorem on the 100 Theorems list? If not, I feel less urgency about the classical formulation.