Heather Macbeth
Heather Macbeth
In the doc-gen for mathlib3, the left sidebar looks like this: > **core** > ▸ data > ▸ init > ▸ system > > **mathlib** > ▸ algebra > ▸...
This doesn't build, but as far as I can tell it's unrelated to the typo fix I made.
In the section "Hilbert spaces" of the `undergrad.yaml` file, there are two entries called "its completeness". It makes sense in context: ```yaml ... dual space: 'normed_space.dual.normed_space' Riesz representation theorem: 'inner_product_space.to_dual'...
### Proposal Currently, if multiple constructors of an inductive type are applicable to a goal, the `constructor` tactic will apply the first one which works. The proposal is to instead...
The Mathlib `have` tactic does not seem to be supported yet, is that right? The following two code snippets are mathematically equivalent, as far as I'm concerned, and it would...
The `calc` tactic has a slightly distracting Paperproof display which privileges the first line of the calc (printing this explicitly) over the later lines. Term-mode `calc` does not seem to...
At the moment, the Lean 4 VS Code extension reports "Goals accomplished 🎉" if the goal list is empty. This is copied from the Lean 3 behaviour (https://github.com/leanprover/vscode-lean/pull/114). However, far...
Goals `a ≠ b` turn up quite often when working over general fields, notably goals `a ≠ 0` to allow for the use of `field_simp` with a denominator `a`. Often...
A Lipschitz function from a subset of a space into ℓ^∞ can be extended to the whole space, with the same Lipschitz constant. See Theorem 2.2 here: https://web.math.princeton.edu/~naor/homepage%20files/embeddings_extensions.pdf We have...
Feel free to decline this if you prefer to do it yourself! I made a v4.22.0 version because I wanted to try it with the latest version of Verso.