Theorem IsUltrametricDist.exists_norm_finset_prod_le_of_nonempty

Modification history

2024-10-21 14:44
Mathlib/Analysis/Normed/Group/Ultra.lean
feat(Data/Real/IsNonarchimedean): add lemmas (#16767) …
Added IsUltrametricDist.exists_norm_finset_prod_le_of_nonemptyView on Github →