search

metamath / set.mm

Metamath source file for logic and set theory
Other
243 stars 88 forks source link

'Norm' in a pointed set. #4167

Closed benjub closed 2 weeks ago

benjub commented 2 weeks ago

While proofreading a section comment in a recent PR, I noticed that it was natural to add this generalization and that it clarified the exposition.