∀ {ι : Type u_1} {G : Type u_2} [inst : AddGroup G] [inst_1 : ConditionallyCompleteLattice G] [Nonempty ι] {f : ι → G}
  [AddRightMono G], BddBelow (Set.range f) → ∀ (a : G), (⨅ i, f i) - a = ⨅ i, f i - a