Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-18 14:23 5859ec0f

View on Github →

feat(analysis/normed_space/lattice_ordered_group): prove order_closed_topology for normed_lattice_add_comm_group (#10838)

Estimated changes

added theorem continuous_neg'
added theorem continuous_pos
added theorem is_closed_nonneg
added theorem lipschitz_with_pos