Theorem Nontrivial.of_nontrivialTopology

Modification history

2026-05-19 19:46
Mathlib/Topology/Order.lean
feat(Analysis): operator norm of a `LinearIsometryEquiv` (#39143) …
Added Nontrivial.of_nontrivialTopologyView on Github →