Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-03-14 03:45
1d68cc90
View on Github →
feat: port Analysis.Normed.Order.Lattice (
#2851
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Analysis/Normed/Order/Lattice.lean
added
theorem
continuous_neg'
added
theorem
continuous_pos
added
theorem
dual_solid
added
theorem
isClosed_le_of_isClosed_nonneg
added
theorem
isClosed_nonneg
added
theorem
lipschitzWith_pos
added
theorem
lipschitzWith_sup_right
added
theorem
norm_abs_eq_norm
added
theorem
norm_abs_sub_abs
added
theorem
norm_inf_le_add
added
theorem
norm_inf_sub_inf_le_add_norm
added
theorem
norm_inf_sub_inf_le_norm
added
theorem
norm_sup_le_add
added
theorem
norm_sup_sub_sup_le_add_norm
added
theorem
norm_sup_sub_sup_le_norm
added
theorem
solid