egauge_le_of_smul_mem — Mathlib

English

A variant of the pi-index gauge inequality holds with nonempty assumptions.

Русский

Существует вариант неравенства гейдж для индекса Π с ненулевыми предположениями.

LaTeX

$$$\ldots$$$

Lean4

/-- If `c • x ∈ s`, then `egauge 𝕜 s x` is at most `‖c‖ₑ⁻¹`.

See also `egauge_le_of_smul_mem_of_ne`. -/
theorem egauge_le_of_smul_mem (h : c • x ∈ s) : egauge 𝕜 s x ≤ ‖c‖ₑ⁻¹ :=
  by
  rcases eq_or_ne c 0 with rfl | hc
  · simp
  · exact (egauge_le_of_smul_mem_of_ne h hc).trans ENNReal.coe_inv_le

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