le_ciInf_add_ciInf

theorem le_ciInf_add_ciInf : ∀ {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [inst : Nonempty ι] [inst : Nonempty ι'] [inst : ConditionallyCompleteLattice α] [inst_1 : AddGroup α] [inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {g : ι → α} {h : ι' → α}, (∀ (i : ι) (j : ι'), a ≤ g i + h j) → a ≤ iInf g + iInf h

This theorem states that for any types `α`, `ι`, and `ι'`, given that `ι` and `ι'` are both nonempty and `α` forms a conditionally complete lattice and an additive group, and if `α` has the property that for any two elements `x` and `x_1`, the operation `(x + x_1)` is covariant with respect to the order relation `≤` (both when considered in the usual order and when the operation is swapped), then for any element `a` of `α` and any two functions `g : ι → α` and `h : ι' → α`, if `a` is less than or equal to the sum of `g i` and `h j` for any `i` in `ι` and `j` in `ι'`, then `a` is also less than or equal to the infimum of the range of `g` plus the infimum of the range of `h`. In mathematical terms, if `a ≤ g(i) + h(j)` for all `i` and `j`, then `a ≤ inf g + inf h`, where `inf` denotes the infimum (greatest lower bound) over the range of the function.

More concisely: If `α` is a conditionally complete lattice and additive group, `ι` and `ι'` are nonempty, `a ≤ g(i) + h(j)` for all `i ∈ ι` and `j ∈ ι'`, and the addition operation is covariant with respect to the order relation `≤` in `α`, then `a ≤ inf(g) + inf(h)`.