Theorem nnreal.coe_Sup
Modification history
2022-04-19 17:41
src/data/real/nnreal.lean
feat(analysis): lemmas about nnnorm and nndist (#13498) …
Modified nnreal.coe_SupView on Github →2021-08-02 02:56
src/data/real/nnreal.lean
refactor(data/real/nnreal): use `ord_connected_subset_conditionally_complete_linear_order` (#8502)
Modified nnreal.coe_SupView on Github →