le_egauge_pi — Mathlib

English

The egauge of a product set dominates the maxima of the egauges of the factors.

Русский

Гейдж произведения множества доминирует над максимумами гейджей факторов.

LaTeX

$$$\max(\mathrm{egauge}_{\mathbb{K}}(s,a),\mathrm{egauge}_{\mathbb{K}}(t,b)) \le \mathrm{egauge}_{\mathbb{K}}(s \times\! t)(a,b)$$$

Lean4

theorem le_egauge_pi {ι : Type*} {E : ι → Type*} [∀ i, SMul 𝕜 (E i)] {I : Set ι} {i : ι} (hi : i ∈ I)
    (s : ∀ i, Set (E i)) (x : ∀ i, E i) : egauge 𝕜 (s i) (x i) ≤ egauge 𝕜 (I.pi s) x :=
  MapsTo.egauge_le _ (Pi.evalMulActionHom i) (fun x hx ↦ by exact hx i hi) _

Похожие утверждения