Wrenna Robson

feat(topology/metric_space/infsep): Add "infimum separation".

3

Informally, this is the "minimum distance", though "minimum" makes sense mainly only in the finite context. This is analogous to diam in some sense. We provide finset and set versions...

refactor(algebra/order/floor): Relax lemmas to remove `linear_order` requirement

13

There is a TODO in `algebra/order/floor.lean` which notes that many lemmas do not require the linearly ordered part of their hypothesis and these could be relaxed. This commit actions this...

https://staging.bsky.app/profile/ resolves to the BSky profile for @, if present. https://staging.bsky.app/profile// does not - it returns a 404. Other social sites make it work differently (I assume it's a simple...

fix: remove `Option.lt` and related components

13

--- This is a draft PR implementing the minimal changes required to fix #3100.

fix: Add missing csimp lemma

5

Addresses issue [batteries#307](https://github.com/leanprover-community/batteries/issues/307). Closes #307

I am not sure if this is ultimately a mathlib or batteries issue but I have been advised to post this here. See the discussion at the end of https://leanprover.zulipchat.com/#narrow/channel/348111-batteries/topic/Chain.20and.20Chain'.20and.20Pairwise/with/540902002...