Mathlib v3 is deprecated. Go to Mathlib v4

Theorem norm_two_inf_sub_two_inf_le

Modification history

2021-12-05 11:46
src/analysis/normed_space/lattice_ordered_group.lean
feat(topology/continuous_function/bounded): continuous bounded real-valued functions form a normed vector lattice (#10322) …
Deleted norm_two_inf_sub_two_inf_leView on Github →
2021-12-03 20:46
src/analysis/normed_space/lattice_ordered_group.lean
feat(analysis.normed_space.lattice_ordered_group): Add `two_inf_sub_two_inf_le`, `two_sup_sub_two_sup_le` and supporting lemmas (#10514) …
Added norm_two_inf_sub_two_inf_leView on Github →