Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-05-11 05:57 5dc275ec

View on Github →

feat(analysis/normed/order/lattice): add has_solid_norm (#18554) See this Zulip thread

Estimated changes

Modified src/algebra/order/lattice_group.lean

added def lattice_ordered_add_comm_group.is_solid

added theorem lattice_ordered_add_comm_group.is_solid_solid_closure

added def lattice_ordered_add_comm_group.solid_closure

added theorem lattice_ordered_add_comm_group.solid_closure_min

Modified src/analysis/normed/order/lattice.lean

added theorem lattice_ordered_add_comm_group.is_solid_ball

added theorem norm_le_norm_of_abs_le_abs

deleted theorem solid

Modified src/measure_theory/function/lp_order.lean

Modified src/topology/continuous_function/bounded.lean