Mathlib v3 is deprecated. Go to Mathlib v4

Theorem lattice_ordered_add_comm_group.is_solid_ball

Modification history

2023-05-11 05:57
src/analysis/normed/order/lattice.lean
feat(analysis/normed/order/lattice): add has_solid_norm (#18554) …
Added lattice_ordered_add_comm_group.is_solid_ballView on Github →