le_egauge_prod — Mathlib

English

For a product index, the gauge respects product structure through the evaluation maps.

Русский

Для произведения индексов гейдж учитывает структуру произведения через отображения выборки.

LaTeX

$$$\text{le_egauge_pi} \text{(variant)}$$$

Lean4

theorem le_egauge_prod (s : Set E) (t : Set F) (a : E) (b : F) :
    max (egauge 𝕜 s a) (egauge 𝕜 t b) ≤ egauge 𝕜 (s ×ˢ t) (a, b) :=
  max_le (mapsTo_fst_prod.egauge_le 𝕜 (MulActionHom.fst 𝕜 E F) (a, b))
    (MapsTo.egauge_le 𝕜 (MulActionHom.snd 𝕜 E F) mapsTo_snd_prod (a, b))

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