mem_smul_of_egauge_lt — Mathlib

English

If a smul inequality holds for egauge, then the corresponding membership holds.

Русский

Если выполняется неравенство смула для egauge, то соответствующее членство верно.

LaTeX

$$$\text{…}$$$

Lean4

theorem mem_smul_of_egauge_lt (hs : Balanced 𝕜 s) (hc : egauge 𝕜 s x < ‖c‖ₑ) : x ∈ c • s :=
  let ⟨a, hxa, ha⟩ := egauge_lt_iff.1 hc
  hs.smul_mono (by simpa [enorm] using ha.le) hxa

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