Hi Ross!
Thanks for pointing it out, this is now fixed.
BR,
_
Thierry
On 14/07/2025 01:59, Tang Ross wrote:
In https://metamath.tirix.org/mpests/df-inf, it shows,
And if I mouse over the first sup, the url is actually
https://metamath.tirix.org/mpests/df-inf.
Showing it as ascii also reveal,
Assertion
df-inf <https://metamath.tirix.org/mpeascii/df-inf#> |- inf ( A , B ,
R ) = sup ( A , B , `' R )
--
You received this message because you are subscribed to the Google
Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send
an email to [email protected].
To view this discussion visit
https://groups.google.com/d/msgid/metamath/9cbaf8ef-728f-47e0-8f5f-ece87dd65fdbn%40googlegroups.com
<https://groups.google.com/d/msgid/metamath/9cbaf8ef-728f-47e0-8f5f-ece87dd65fdbn%40googlegroups.com?utm_medium=email&utm_source=footer>.
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion visit
https://groups.google.com/d/msgid/metamath/0e5bc610-6c8c-46ff-ac66-c98fe563bc36%40gmx.net.
