analysis icon indicating copy to clipboard operation
analysis copied to clipboard

Published 20 hours ago • verified publisher icon math-comp

\near F, P F

Open affeldt-aist opened this issue 3 years ago • 2 comments

https://github.com/math-comp/analysis/blob/ceb11bd28d7a43f63238cd0f9039953059f097a3/theories/topology.v#L133

~~should be \forall y \near x, P y~~ taken care of by PR #782

affeldt-aist avatar Oct 17 '22 08:10 affeldt-aist

It also looks like \forall x \near F, P x always displays as \near F, P F (unless F is a composed expression such as nbhs X or f @ X or a defined expression such as \oo).

affeldt-aist avatar Oct 17 '22 08:10 affeldt-aist

side question: would it be bad to get rid of the \near F, P F?

affeldt-aist avatar Oct 19 '22 14:10 affeldt-aist