Module docstring
{"# Conditionally complete lattices and groups.
"}
ciSup_mul_le_ciSup_mul_ciSup
theorem
[MulLeftMono α] [MulRightMono α] {f g : ι → α} (hf : BddAbove (range f)) (hg : BddAbove (range g)) :
⨆ i, f i * g i ≤ (⨆ i, f i) * ⨆ i, g i
Full source
@[to_additive]
lemma ciSup_mul_le_ciSup_mul_ciSup [MulLeftMono α] [MulRightMono α]
{f g : ι → α} (hf : BddAbove (range f)) (hg : BddAbove (range g)) :
⨆ i, f i * g i ≤ (⨆ i, f i) * ⨆ i, g i :=
ciSup_le fun i ↦ mul_le_mul' (le_ciSup hf i) (le_ciSup hg i)Informal description
Let $\alpha$ be a conditionally complete lattice with multiplication operations that are monotone in both arguments. For any functions $f, g : \iota \to \alpha$ with bounded ranges, the supremum of the pointwise products satisfies:
\[ \bigsqcup_{i \in \iota} (f(i) \cdot g(i)) \leq \left(\bigsqcup_{i \in \iota} f(i)\right) \cdot \left(\bigsqcup_{i \in \iota} g(i)\right). \]
ciInf_mul_ciInf_le_ciInf_mul
theorem
[MulLeftMono α] [MulRightMono α] {f g : ι → α} (hf : BddBelow (range f)) (hg : BddBelow (range g)) :
(⨅ i, f i) * ⨅ i, g i ≤ ⨅ i, f i * g i
Full source
@[to_additive]
lemma ciInf_mul_ciInf_le_ciInf_mul [MulLeftMono α] [MulRightMono α]
{f g : ι → α} (hf : BddBelow (range f)) (hg : BddBelow (range g)) :
(⨅ i, f i) * ⨅ i, g i ≤ ⨅ i, f i * g i :=
le_ciInf fun i ↦ mul_le_mul' (ciInf_le hf i) (ciInf_le hg i)Informal description
Let $\alpha$ be a conditionally complete lattice with multiplication operations that are monotone in both arguments. For any functions $f, g : \iota \to \alpha$ with bounded below ranges, the product of the infima satisfies:
\[ \left(\bigsqcap_{i \in \iota} f(i)\right) \cdot \left(\bigsqcap_{i \in \iota} g(i)\right) \leq \bigsqcap_{i \in \iota} (f(i) \cdot g(i)). \]
le_mul_ciInf
theorem
[MulLeftMono α] {a : α} {g : α} {h : ι → α} (H : ∀ j, a ≤ g * h j) : a ≤ g * iInf h
Full source
@[to_additive]
theorem le_mul_ciInf [MulLeftMono α] {a : α} {g : α} {h : ι → α}
(H : ∀ j, a ≤ g * h j) : a ≤ g * iInf h :=
inv_mul_le_iff_le_mul.mp <| le_ciInf fun _ => inv_mul_le_iff_le_mul.mpr <| H _Informal description
Let $\alpha$ be a conditionally complete lattice with a multiplication operation that is monotone in its left argument. For any element $a \in \alpha$, any element $g \in \alpha$, and any function $h : \iota \to \alpha$, if $a \leq g \cdot h(j)$ for all $j \in \iota$, then $a \leq g \cdot \bigsqcap_{i \in \iota} h(i)$.
mul_ciSup_le
theorem
[MulLeftMono α] {a : α} {g : α} {h : ι → α} (H : ∀ j, g * h j ≤ a) : g * iSup h ≤ a
Full source
@[to_additive]
theorem mul_ciSup_le [MulLeftMono α] {a : α} {g : α} {h : ι → α}
(H : ∀ j, g * h j ≤ a) : g * iSup h ≤ a :=
le_mul_ciInf (α := αᵒᵈ) HInformal description
Let $\alpha$ be a conditionally complete lattice with a multiplication operation that is monotone in its left argument. For any elements $a, g \in \alpha$ and any function $h : \iota \to \alpha$, if $g \cdot h(j) \leq a$ for all $j \in \iota$, then $g \cdot \bigsqcup_{i \in \iota} h(i) \leq a$.
le_ciInf_mul
theorem
[MulRightMono α] {a : α} {g : ι → α} {h : α} (H : ∀ i, a ≤ g i * h) : a ≤ iInf g * h
Full source
@[to_additive]
theorem le_ciInf_mul [MulRightMono α] {a : α} {g : ι → α}
{h : α} (H : ∀ i, a ≤ g i * h) : a ≤ iInf g * h :=
mul_inv_le_iff_le_mul.mp <| le_ciInf fun _ => mul_inv_le_iff_le_mul.mpr <| H _Informal description
Let $\alpha$ be a conditionally complete lattice with a multiplication operation that is monotone in its right argument. For any element $a \in \alpha$, any function $g : \iota \to \alpha$, and any element $h \in \alpha$, if $a \leq g(i) \cdot h$ for all $i \in \iota$, then $a \leq \left(\bigsqcap_{i \in \iota} g(i)\right) \cdot h$.
ciSup_mul_le
theorem
[MulRightMono α] {a : α} {g : ι → α} {h : α} (H : ∀ i, g i * h ≤ a) : iSup g * h ≤ a
Full source
@[to_additive]
theorem ciSup_mul_le [MulRightMono α] {a : α} {g : ι → α}
{h : α} (H : ∀ i, g i * h ≤ a) : iSup g * h ≤ a :=
le_ciInf_mul (α := αᵒᵈ) HInformal description
Let $\alpha$ be a conditionally complete lattice with a multiplication operation that is monotone in its right argument. For any element $a \in \alpha$, any function $g : \iota \to \alpha$, and any element $h \in \alpha$, if $g(i) \cdot h \leq a$ for all $i \in \iota$, then $\left(\bigsqcup_{i \in \iota} g(i)\right) \cdot h \leq a$.
le_ciInf_mul_ciInf
theorem
[MulLeftMono α] [MulRightMono α] {a : α} {g : ι → α} {h : ι' → α} (H : ∀ i j, a ≤ g i * h j) : a ≤ iInf g * iInf h
Full source
@[to_additive]
theorem le_ciInf_mul_ciInf [MulLeftMono α] [MulRightMono α] {a : α} {g : ι → α} {h : ι' → α}
(H : ∀ i j, a ≤ g i * h j) : a ≤ iInf g * iInf h :=
le_ciInf_mul fun _ => le_mul_ciInf <| H _Informal description
Let $\alpha$ be a conditionally complete lattice with a multiplication operation that is monotone in both left and right arguments. For any element $a \in \alpha$, any function $g : \iota \to \alpha$, and any function $h : \iota' \to \alpha$, if $a \leq g(i) \cdot h(j)$ for all $i \in \iota$ and $j \in \iota'$, then $a \leq \left(\bigsqcap_{i \in \iota} g(i)\right) \cdot \left(\bigsqcap_{j \in \iota'} h(j)\right)$.
ciSup_mul_ciSup_le
theorem
[MulLeftMono α] [MulRightMono α] {a : α} {g : ι → α} {h : ι' → α} (H : ∀ i j, g i * h j ≤ a) : iSup g * iSup h ≤ a
Full source
@[to_additive]
theorem ciSup_mul_ciSup_le [MulLeftMono α] [MulRightMono α] {a : α} {g : ι → α} {h : ι' → α}
(H : ∀ i j, g i * h j ≤ a) : iSup g * iSup h ≤ a :=
ciSup_mul_le fun _ => mul_ciSup_le <| H _Informal description
Let $\alpha$ be a conditionally complete lattice with a multiplication operation that is monotone in both left and right arguments. For any element $a \in \alpha$, any function $g : \iota \to \alpha$, and any function $h : \iota' \to \alpha$, if $g(i) \cdot h(j) \leq a$ for all $i \in \iota$ and $j \in \iota'$, then $\left(\bigsqcup_{i \in \iota} g(i)\right) \cdot \left(\bigsqcup_{j \in \iota'} h(j)\right) \leq a$.