egauge_le — Mathlib

English

If a map f sends s into t, then egauge_t(f(x)) ≤ egauge_s(x).

Русский

Если отображение f отправляет s в t, то egauge_t(f(x)) ≤ egauge_s(x).

LaTeX

$$$\mathrm{MapsTo}\ f\ s\ t \Rightarrow \forall x, \mathrm{egauge}_{\mathbb{K}}(t, f(x)) \le \mathrm{egauge}_{\mathbb{K}}(s, x)$$$

Lean4

theorem egauge_le {E' F : Type*} [SMul 𝕜 E'] [FunLike F E E'] [MulActionHomClass F 𝕜 E E'] (f : F) {t : Set E'}
    (h : MapsTo f s t) (x : E) : egauge 𝕜 t (f x) ≤ egauge 𝕜 s x :=
  iInf_mono fun c ↦ iInf_mono' fun hc ↦ ⟨h.smul_set c hc, le_rfl⟩

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