mathlib

mathlib copied to clipboard

---

I think this is helpful. Although I understand @erdOne 's hesitation. @adamtopaz what do you think?

To be honest, this notation looks quite awkward. And since it's not too similar (unless you really squint) to what we would write on paper, I'm not sure if it's worth adding this notation right now. Maybe Lean4 would let us introduce better notation? If so, perhaps we should just wait until the port to Lean4?

There are two notations introduced.

• x ∣_ₕ e for F.map e.op x
• x ∣_ₗ V ⟪e⟫ for F.map (hom_of_le e).op x

Are you referring to both of them? Although I agree that this is quite awkward, I think we would always need to provide the proof that V ≤ U nonetheless, and I'm not sure (due to the lack of knowledge regarding Lean4) if Lean4 could help the situation.

:v: erdOne can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

bors merge

Build failed (retrying...):

• Lint mathlib

Build failed (retrying...):

• Run tests

I think we would always need to provide the proof that V ≤ U nonetheless

Do you know you can already make the notation infer the proof? Something like

notation ` fin_mk ` k := fin.mk _ ‹k < n›

Build failed (retrying...):

• Run tests

Ah I forgot about that. We will probably need a custom tactic instead but this is definitely worth a try.

bors cancel Let me experiment with that a bit.

Canceled.

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests