Mathlib.Data.NNReal.Basic

NNReal.instFloorSemiring instance

: FloorSemiring ℝ≥0

Full source

noncomputable instance : FloorSemiring ℝ≥0 := Nonneg.floorSemiring

Floor Semiring Structure on Non-Negative Real Numbers

Informal description

The non-negative real numbers $\mathbb{R}_{\geq 0}$ form a floor semiring, inheriting the floor function structure from the real numbers $\mathbb{R}$.

NNReal.coe_indicator theorem

 {α} (s : Set α) (f : α → ℝ≥0) (a : α) : ((s.indicator f a : ℝ≥0) : ℝ) = s.indicator (fun x => ↑(f x)) a

Full source

@[simp, norm_cast]
theorem coe_indicator {α} (s : Set α) (f : α → ℝ≥0) (a : α) :
    ((s.indicator f a : ℝ≥0) : ℝ) = s.indicator (fun x => ↑(f x)) a :=
  (toRealHom : ℝ≥0ℝ≥0 →+ ℝ).map_indicator _ _ _

Compatibility of Non-Negative Real Inclusion with Indicator Functions

Informal description

For any set $s$ over a type $\alpha$ and any function $f \colon \alpha \to \mathbb{R}_{\geq 0}$, the canonical inclusion map from non-negative reals to reals commutes with the set indicator function. That is, for any $a \in \alpha$, we have: $$(s.\text{indicator}\,f\,a) = s.\text{indicator}\,(\lambda x \mapsto f(x))\,a$$ where the left side is interpreted in $\mathbb{R}$ and the right side is interpreted in $\mathbb{R}_{\geq 0}$.

NNReal.coe_list_sum theorem

(l : List ℝ≥0) : ((l.sum : ℝ≥0) : ℝ) = (l.map (↑)).sum

Full source

@[norm_cast]
theorem coe_list_sum (l : List ℝ≥0) : ((l.sum : ℝ≥0) : ℝ) = (l.map (↑)).sum :=
  map_list_sum toRealHom l

Sum Preservation Under Inclusion of Non-Negative Real Numbers

Informal description

For any list $l$ of non-negative real numbers, the canonical inclusion map applied to the sum of $l$ equals the sum of the list obtained by applying the canonical inclusion map to each element of $l$. In other words, if $\iota : \mathbb{R}_{\geq 0} \to \mathbb{R}$ is the inclusion map, then $\iota(\sum l) = \sum (\iota \circ l)$.

NNReal.coe_list_prod theorem

(l : List ℝ≥0) : ((l.prod : ℝ≥0) : ℝ) = (l.map (↑)).prod

Full source

@[norm_cast]
theorem coe_list_prod (l : List ℝ≥0) : ((l.prod : ℝ≥0) : ℝ) = (l.map (↑)).prod :=
  map_list_prod toRealHom l

Canonical Inclusion Preserves List Products: $\left(\prod l\right)_{\mathbb{R}} = \prod (l_{\mathbb{R}})$

Informal description

For any list $l$ of non-negative real numbers, the canonical inclusion of the product of $l$ (as an element of $\mathbb{R}_{\geq 0}$) into $\mathbb{R}$ equals the product of the list obtained by applying the canonical inclusion to each element of $l$. In symbols: $$ \left(\prod_{x \in l} x\right)_{\mathbb{R}} = \prod_{x \in l} x_{\mathbb{R}} $$ where $x_{\mathbb{R}}$ denotes the canonical inclusion of $x \in \mathbb{R}_{\geq 0}$ into $\mathbb{R}$.

NNReal.coe_multiset_sum theorem

(s : Multiset ℝ≥0) : ((s.sum : ℝ≥0) : ℝ) = (s.map (↑)).sum

Full source

@[norm_cast]
theorem coe_multiset_sum (s : Multiset ℝ≥0) : ((s.sum : ℝ≥0) : ℝ) = (s.map (↑)).sum :=
  map_multiset_sum toRealHom s

Sum of Non-Negative Real Multiset Preserves Canonical Inclusion

Informal description

For any multiset $s$ of non-negative real numbers (elements of $\mathbb{R}_{\geq 0}$), the canonical inclusion of the sum of $s$ in $\mathbb{R}_{\geq 0}$ equals the sum in $\mathbb{R}$ of the multiset obtained by applying the canonical inclusion to each element of $s$. In symbols: $$ \left(\sum s : \mathbb{R}_{\geq 0}\right) = \sum_{x \in s} (x : \mathbb{R}) $$

NNReal.coe_multiset_prod theorem

(s : Multiset ℝ≥0) : ((s.prod : ℝ≥0) : ℝ) = (s.map (↑)).prod

Full source

@[norm_cast]
theorem coe_multiset_prod (s : Multiset ℝ≥0) : ((s.prod : ℝ≥0) : ℝ) = (s.map (↑)).prod :=
  map_multiset_prod toRealHom s

Canonical Inclusion Preserves Multiset Product in Non-Negative Reals

Informal description

For any multiset $s$ of non-negative real numbers, the canonical inclusion of the product of $s$ (as an element of $\mathbb{R}_{\geq 0}$) into $\mathbb{R}$ equals the product of the multiset obtained by applying the canonical inclusion to each element of $s$. In symbols: $$ \left(\prod s : \mathbb{R}_{\geq 0}\right)_{\mathbb{R}} = \prod_{x \in s} (x : \mathbb{R}) $$

NNReal.coe_sum theorem

(s : Finset ι) (f : ι → ℝ≥0) : ∑ i ∈ s, f i = ∑ i ∈ s, (f i : ℝ)

Full source

@[simp, norm_cast]
theorem coe_sum (s : Finset ι) (f : ι → ℝ≥0) : ∑ i ∈ s, f i = ∑ i ∈ s, (f i : ℝ) :=
  map_sum toRealHom _ _

Sum of Non-Negative Real Numbers Equals Sum in Reals

Informal description

For any finite set $s$ and any function $f$ from $s$ to the non-negative real numbers $\mathbb{R}_{\geq 0}$, the sum of $f$ over $s$ in $\mathbb{R}_{\geq 0}$ is equal to the sum of $f$ over $s$ in $\mathbb{R}$ when each term is considered as a real number.

NNReal.coe_expect theorem

(s : Finset ι) (f : ι → ℝ≥0) : 𝔼 i ∈ s, f i = 𝔼 i ∈ s, (f i : ℝ)

Full source

@[simp, norm_cast]
lemma coe_expect (s : Finset ι) (f : ι → ℝ≥0) : 𝔼 i ∈ s, f i = 𝔼 i ∈ s, (f i : ℝ) :=
  map_expect toRealHom ..

Equality of Expectations for Non-Negative Real-Valued Functions

Informal description

For any finite set $s$ and any function $f$ from $s$ to the non-negative real numbers $\mathbb{R}_{\geq 0}$, the expectation of $f$ over $s$ (considered as a non-negative real number) is equal to the expectation of the real-valued function obtained by composing $f$ with the inclusion map $\mathbb{R}_{\geq 0} \hookrightarrow \mathbb{R}$.

Real.toNNReal_sum_of_nonneg theorem

(hf : ∀ i ∈ s, 0 ≤ f i) : Real.toNNReal (∑ a ∈ s, f a) = ∑ a ∈ s, Real.toNNReal (f a)

Full source

theorem _root_.Real.toNNReal_sum_of_nonneg (hf : ∀ i ∈ s, 0 ≤ f i) :
    Real.toNNReal (∑ a ∈ s, f a) = ∑ a ∈ s, Real.toNNReal (f a) := by
  rw [← coe_inj, NNReal.coe_sum, Real.coe_toNNReal _ (Finset.sum_nonneg hf)]
  exact Finset.sum_congr rfl fun x hxs => by rw [Real.coe_toNNReal _ (hf x hxs)]

Non-negative part of sum equals sum of non-negative parts for non-negative functions

Informal description

For any finite set $s$ and any function $f$ from $s$ to the real numbers such that $f(i) \geq 0$ for all $i \in s$, the non-negative part of the sum of $f$ over $s$ equals the sum of the non-negative parts of $f$ over $s$. That is, $$\text{toNNReal}\left(\sum_{a \in s} f(a)\right) = \sum_{a \in s} \text{toNNReal}(f(a)).$$

NNReal.coe_prod theorem

(s : Finset ι) (f : ι → ℝ≥0) : ↑(∏ a ∈ s, f a) = ∏ a ∈ s, (f a : ℝ)

Full source

@[simp, norm_cast]
theorem coe_prod (s : Finset ι) (f : ι → ℝ≥0) : ↑(∏ a ∈ s, f a) = ∏ a ∈ s, (f a : ℝ) :=
  map_prod toRealHom _ _

Inclusion Map Preserves Finite Products of Non-Negative Reals

Informal description

For any finite set $s$ and any function $f : \iota \to \mathbb{R}_{\geq 0}$, the canonical inclusion map from non-negative reals to reals preserves the product over $s$. That is, the image of the product $\prod_{a \in s} f(a)$ under the inclusion map is equal to the product $\prod_{a \in s} (f(a) : \mathbb{R})$.

Real.toNNReal_prod_of_nonneg theorem

(hf : ∀ a, a ∈ s → 0 ≤ f a) : Real.toNNReal (∏ a ∈ s, f a) = ∏ a ∈ s, Real.toNNReal (f a)

Full source

theorem _root_.Real.toNNReal_prod_of_nonneg (hf : ∀ a, a ∈ s → 0 ≤ f a) :
    Real.toNNReal (∏ a ∈ s, f a) = ∏ a ∈ s, Real.toNNReal (f a) := by
  rw [← coe_inj, NNReal.coe_prod, Real.coe_toNNReal _ (Finset.prod_nonneg hf)]
  exact Finset.prod_congr rfl fun x hxs => by rw [Real.coe_toNNReal _ (hf x hxs)]

Non-negative Part Preserves Finite Products of Non-negative Reals

Informal description

For any finite set $s$ and any function $f$ defined on $s$ such that $f(a) \geq 0$ for all $a \in s$, the non-negative part of the product $\prod_{a \in s} f(a)$ is equal to the product of the non-negative parts of $f(a)$ over $s$, i.e., \[ \text{toNNReal}\left(\prod_{a \in s} f(a)\right) = \prod_{a \in s} \text{toNNReal}(f(a)). \]

NNReal.le_iInf_add_iInf theorem

 {ι ι' : Sort*} [Nonempty ι] [Nonempty ι'] {f : ι → ℝ≥0} {g : ι' → ℝ≥0} {a : ℝ≥0} (h : ∀ i j, a ≤ f i + g j) :
  a ≤ (⨅ i, f i) + ⨅ j, g j

Full source

theorem le_iInf_add_iInf {ι ι' : Sort*} [Nonempty ι] [Nonempty ι'] {f : ι → ℝ≥0} {g : ι' → ℝ≥0}
    {a : ℝ≥0} (h : ∀ i j, a ≤ f i + g j) : a ≤ (⨅ i, f i) + ⨅ j, g j := by
  rw [← NNReal.coe_le_coe, NNReal.coe_add, coe_iInf, coe_iInf]
  exact le_ciInf_add_ciInf h

Infimum Sum Inequality for Non-Negative Reals: $a \leq \inf f + \inf g$ under pointwise bounds

Informal description

Let $\{f_i\}_{i \in \iota}$ and $\{g_j\}_{j \in \iota'}$ be two families of non-negative real numbers, where $\iota$ and $\iota'$ are nonempty index types. If for every $i \in \iota$ and $j \in \iota'$, a non-negative real number $a$ satisfies $a \leq f_i + g_j$, then $a$ is less than or equal to the sum of the infima of the two families, i.e., \[ a \leq \left(\inf_{i} f_i\right) + \inf_{j} g_j. \]

NNReal.mul_finset_sup theorem

{α} (r : ℝ≥0) (s : Finset α) (f : α → ℝ≥0) : r * s.sup f = s.sup fun a => r * f a

Full source

theorem mul_finset_sup {α} (r : ℝ≥0) (s : Finset α) (f : α → ℝ≥0) :
    r * s.sup f = s.sup fun a => r * f a :=
  Finset.comp_sup_eq_sup_comp _ (NNReal.mul_sup r) (mul_zero r)

Distributivity of multiplication over finite supremum in non-negative reals: $r \cdot \sup f = \sup (r \cdot f)$

Informal description

For any non-negative real number $r$ and any finite set $s$ of elements of type $\alpha$, and for any function $f : \alpha \to \mathbb{R}_{\geq 0}$, the product of $r$ with the supremum of $f$ over $s$ is equal to the supremum of the function $a \mapsto r \cdot f(a)$ over $s$, i.e., \[ r \cdot \sup_{a \in s} f(a) = \sup_{a \in s} (r \cdot f(a)). \]

NNReal.finset_sup_mul theorem

{α} (s : Finset α) (f : α → ℝ≥0) (r : ℝ≥0) : s.sup f * r = s.sup fun a => f a * r

Full source

theorem finset_sup_mul {α} (s : Finset α) (f : α → ℝ≥0) (r : ℝ≥0) :
    s.sup f * r = s.sup fun a => f a * r :=
  Finset.comp_sup_eq_sup_comp (· * r) (fun x y => NNReal.sup_mul x y r) (zero_mul r)

Distributivity of Supremum over Multiplication in Non-Negative Reals: $(\sup f) \cdot r = \sup (f \cdot r)$

Informal description

For any finite set $s$ of elements of type $\alpha$, any function $f : \alpha \to \mathbb{R}_{\geq 0}$, and any non-negative real number $r \in \mathbb{R}_{\geq 0}$, the product of the supremum of $f$ over $s$ with $r$ is equal to the supremum of the function $a \mapsto f(a) \cdot r$ over $s$, i.e., \[ \left(\sup_{a \in s} f(a)\right) \cdot r = \sup_{a \in s} (f(a) \cdot r). \]

NNReal.finset_sup_div theorem

{α} {f : α → ℝ≥0} {s : Finset α} (r : ℝ≥0) : s.sup f / r = s.sup fun a => f a / r

Full source

theorem finset_sup_div {α} {f : α → ℝ≥0} {s : Finset α} (r : ℝ≥0) :
    s.sup f / r = s.sup fun a => f a / r := by simp only [div_eq_inv_mul, mul_finset_sup]

Distributivity of Supremum over Division in Non-Negative Reals: $(\sup f) / r = \sup (f / r)$

Informal description

For any finite set $s$ of elements of type $\alpha$, any function $f : \alpha \to \mathbb{R}_{\geq 0}$, and any non-negative real number $r \in \mathbb{R}_{\geq 0}$, the quotient of the supremum of $f$ over $s$ by $r$ is equal to the supremum of the function $a \mapsto f(a) / r$ over $s$, i.e., \[ \frac{\sup_{a \in s} f(a)}{r} = \sup_{a \in s} \left(\frac{f(a)}{r}\right). \]

NNReal.sub_div theorem

(a b c : ℝ≥0) : (a - b) / c = a / c - b / c

Full source

theorem sub_div (a b c : ℝ≥0) : (a - b) / c = a / c - b / c :=
  tsub_div _ _ _

Subtraction-Division Distributivity for Non-Negative Real Numbers

Informal description

For any non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0}$, the equality $(a - b)/c = a/c - b/c$ holds.

NNReal.iInf_mul theorem

(f : ι → ℝ≥0) (a : ℝ≥0) : iInf f * a = ⨅ i, f i * a

Full source

theorem iInf_mul (f : ι → ℝ≥0) (a : ℝ≥0) : iInf f * a = ⨅ i, f i * a := by
  rw [← coe_inj, NNReal.coe_mul, coe_iInf, coe_iInf]
  exact Real.iInf_mul_of_nonneg (NNReal.coe_nonneg _) _

Infimum-Multiplication Commutation for Nonnegative Reals: $(\inf_i f_i) \cdot a = \inf_i (f_i \cdot a)$

Informal description

For any indexed family of non-negative real numbers $(f_i)_{i \in \iota}$ and any non-negative real number $a$, the product of the infimum of the family with $a$ equals the infimum of the products, i.e., \[ \left(\bigwedge_{i} f_i\right) \cdot a = \bigwedge_{i} (f_i \cdot a). \]

NNReal.mul_iInf theorem

(f : ι → ℝ≥0) (a : ℝ≥0) : a * iInf f = ⨅ i, a * f i

Full source

theorem mul_iInf (f : ι → ℝ≥0) (a : ℝ≥0) : a * iInf f = ⨅ i, a * f i := by
  simpa only [mul_comm] using iInf_mul f a

Multiplication-Infimum Commutation for Nonnegative Reals: $a \cdot \inf_i f_i = \inf_i (a \cdot f_i)$

Informal description

For any indexed family of non-negative real numbers $(f_i)_{i \in \iota}$ and any non-negative real number $a$, the product of $a$ with the infimum of the family equals the infimum of the products, i.e., \[ a \cdot \left(\bigwedge_{i} f_i\right) = \bigwedge_{i} (a \cdot f_i). \]

NNReal.mul_iSup theorem

(f : ι → ℝ≥0) (a : ℝ≥0) : (a * ⨆ i, f i) = ⨆ i, a * f i

Full source

theorem mul_iSup (f : ι → ℝ≥0) (a : ℝ≥0) : (a * ⨆ i, f i) = ⨆ i, a * f i := by
  rw [← coe_inj, NNReal.coe_mul, NNReal.coe_iSup, NNReal.coe_iSup]
  exact Real.mul_iSup_of_nonneg (NNReal.coe_nonneg _) _

Multiplication Commutes with Supremum for Nonnegative Reals: $a \cdot \sup_i f_i = \sup_i (a \cdot f_i)$

Informal description

For any non-negative real number $a \in \mathbb{R}_{\geq 0}$ and any indexed family of non-negative real numbers $(f_i)_{i \in \iota}$, the product of $a$ with the supremum of the family equals the supremum of the products, i.e., \[ a \cdot \left(\sup_{i} f_i\right) = \sup_{i} (a \cdot f_i). \]

NNReal.iSup_mul theorem

(f : ι → ℝ≥0) (a : ℝ≥0) : (⨆ i, f i) * a = ⨆ i, f i * a

Full source

theorem iSup_mul (f : ι → ℝ≥0) (a : ℝ≥0) : (⨆ i, f i) * a = ⨆ i, f i * a := by
  rw [mul_comm, mul_iSup]
  simp_rw [mul_comm]

Supremum-Multiplication Commutativity for Nonnegative Reals: $(\sup_i f_i) \cdot a = \sup_i (f_i \cdot a)$

Informal description

For any indexed family of nonnegative real numbers $(f_i)_{i \in \iota}$ and any nonnegative real number $a$, the supremum of the family multiplied by $a$ equals the supremum of each $f_i$ multiplied by $a$, i.e., \[ \left(\sup_{i} f_i\right) \cdot a = \sup_{i} (f_i \cdot a). \]

NNReal.iSup_div theorem

(f : ι → ℝ≥0) (a : ℝ≥0) : (⨆ i, f i) / a = ⨆ i, f i / a

Full source

theorem iSup_div (f : ι → ℝ≥0) (a : ℝ≥0) : (⨆ i, f i) / a = ⨆ i, f i / a := by
  simp only [div_eq_mul_inv, iSup_mul]

Supremum-Division Commutativity for Nonnegative Reals: $(\sup_i f_i) / a = \sup_i (f_i / a)$

Informal description

For any indexed family of nonnegative real numbers $(f_i)_{i \in \iota}$ and any nonzero nonnegative real number $a$, the supremum of the family divided by $a$ equals the supremum of each $f_i$ divided by $a$, i.e., \[ \left(\sup_{i} f_i\right) / a = \sup_{i} (f_i / a). \]

NNReal.mul_iSup_le theorem

{a : ℝ≥0} {g : ℝ≥0} {h : ι → ℝ≥0} (H : ∀ j, g * h j ≤ a) : g * iSup h ≤ a

Full source

theorem mul_iSup_le {a : ℝ≥0} {g : ℝ≥0} {h : ι → ℝ≥0} (H : ∀ j, g * h j ≤ a) : g * iSup h ≤ a := by
  rw [mul_iSup]
  exact ciSup_le' H

Multiplication by Supremum Bound in Nonnegative Reals: $g \cdot \sup_j h_j \leq a$ if $g \cdot h_j \leq a$ for all $j$

Informal description

For any non-negative real numbers $a, g \in \mathbb{R}_{\geq 0}$ and any indexed family of non-negative real numbers $(h_j)_{j \in \iota}$, if $g \cdot h_j \leq a$ for all $j \in \iota$, then $g \cdot \left(\sup_{j} h_j\right) \leq a$.

NNReal.iSup_mul_le theorem

{a : ℝ≥0} {g : ι → ℝ≥0} {h : ℝ≥0} (H : ∀ i, g i * h ≤ a) : iSup g * h ≤ a

Full source

theorem iSup_mul_le {a : ℝ≥0} {g : ι → ℝ≥0} {h : ℝ≥0} (H : ∀ i, g i * h ≤ a) : iSup g * h ≤ a := by
  rw [iSup_mul]
  exact ciSup_le' H

Supremum-Multiplication Bound for Nonnegative Reals: $(\sup_i g_i) \cdot h \leq a$ if $g_i \cdot h \leq a$ for all $i$

Informal description

For any nonnegative real numbers $a, h \in \mathbb{R}_{\geq 0}$ and any indexed family of nonnegative real numbers $(g_i)_{i \in \iota}$, if $g_i \cdot h \leq a$ for all $i \in \iota$, then $\left(\sup_{i} g_i\right) \cdot h \leq a$.

NNReal.iSup_mul_iSup_le theorem

{a : ℝ≥0} {g h : ι → ℝ≥0} (H : ∀ i j, g i * h j ≤ a) : iSup g * iSup h ≤ a

Full source

theorem iSup_mul_iSup_le {a : ℝ≥0} {g h : ι → ℝ≥0} (H : ∀ i j, g i * h j ≤ a) :
    iSup g * iSup h ≤ a :=
  iSup_mul_le fun _ => mul_iSup_le <| H _

Supremum Product Bound for Nonnegative Reals: $(\sup_i g_i)(\sup_j h_j) \leq a$ if $g_i h_j \leq a$ for all $i,j$

Informal description

For any nonnegative real number $a \in \mathbb{R}_{\geq 0}$ and any two indexed families of nonnegative real numbers $(g_i)_{i \in \iota}$ and $(h_j)_{j \in \iota}$, if $g_i \cdot h_j \leq a$ for all $i, j \in \iota$, then $\left(\sup_{i} g_i\right) \cdot \left(\sup_{j} h_j\right) \leq a$.

NNReal.le_mul_iInf theorem

{a : ℝ≥0} {g : ℝ≥0} {h : ι → ℝ≥0} (H : ∀ j, a ≤ g * h j) : a ≤ g * iInf h

Full source

theorem le_mul_iInf {a : ℝ≥0} {g : ℝ≥0} {h : ι → ℝ≥0} (H : ∀ j, a ≤ g * h j) : a ≤ g * iInf h := by
  rw [mul_iInf]
  exact le_ciInf H

Lower Bound for Scaled Infimum in Nonnegative Reals: $a \leq g \cdot \inf_j h_j$ if $a \leq g \cdot h_j$ for all $j$

Informal description

For any nonnegative real numbers $a, g \in \mathbb{R}_{\geq 0}$ and any indexed family of nonnegative real numbers $(h_j)_{j \in \iota}$, if $a \leq g \cdot h_j$ holds for all $j \in \iota$, then $a \leq g \cdot \left(\bigwedge_{j} h_j\right)$.

NNReal.le_iInf_mul theorem

{a : ℝ≥0} {g : ι → ℝ≥0} {h : ℝ≥0} (H : ∀ i, a ≤ g i * h) : a ≤ iInf g * h

Full source

theorem le_iInf_mul {a : ℝ≥0} {g : ι → ℝ≥0} {h : ℝ≥0} (H : ∀ i, a ≤ g i * h) : a ≤ iInf g * h := by
  rw [iInf_mul]
  exact le_ciInf H

Lower Bound for Infimum-Multiplication in Non-Negative Reals: $a \leq (\inf_i g_i) \cdot h$

Informal description

For any non-negative real number $a$, any indexed family of non-negative real numbers $(g_i)_{i \in \iota}$, and any non-negative real number $h$, if $a \leq g_i \cdot h$ holds for all $i \in \iota$, then $a \leq \left(\bigwedge_{i} g_i\right) \cdot h$.

NNReal.le_iInf_mul_iInf theorem

{a : ℝ≥0} {g h : ι → ℝ≥0} (H : ∀ i j, a ≤ g i * h j) : a ≤ iInf g * iInf h

Full source

theorem le_iInf_mul_iInf {a : ℝ≥0} {g h : ι → ℝ≥0} (H : ∀ i j, a ≤ g i * h j) :
    a ≤ iInf g * iInf h :=
  le_iInf_mul fun i => le_mul_iInf <| H i

Lower Bound for Product of Infima in Non-Negative Reals: $a \leq (\inf_i g_i)(\inf_j h_j)$ if $a \leq g_i h_j$ for all $i,j$

Informal description

For any non-negative real number $a$ and any two indexed families of non-negative real numbers $(g_i)_{i \in \iota}$ and $(h_j)_{j \in \iota}$, if $a \leq g_i \cdot h_j$ holds for all $i, j \in \iota$, then $a \leq \left(\bigwedge_{i} g_i\right) \cdot \left(\bigwedge_{j} h_j\right)$.

Notations