Commit 2021-12-03 20:46 1376f53d

View on Github →

feat(analysis.normed_space.lattice_ordered_group): Add two_inf_sub_two_inf_le, two_sup_sub_two_sup_le and supporting lemmas (#10514) feat(analysis.normed_space.lattice_ordered_group): Add two_inf_sub_two_inf_le, two_sup_sub_two_sup_le and supporting lemmas

Estimated changes

Modified src/algebra/lattice_ordered_group.lean

added theorem lattice_ordered_comm_group.abs_abs_div_abs_le

added theorem lattice_ordered_comm_group.abs_inv_comm

added theorem lattice_ordered_comm_group.inf_sq_eq_mul_div_abs_div

deleted theorem lattice_ordered_comm_group.two_inf_eq_mul_div_abs_div

Modified src/analysis/normed_space/lattice_ordered_group.lean

added theorem norm_abs_sub_abs

added theorem norm_two_inf_sub_two_inf_le

added theorem norm_two_sup_sub_two_sup_le