egauge_le_of_smul_mem_of_ne — Mathlib

English

If x ∈ s⋅c and c ≠ 0, then x ∈ c·s. (Equivalent formulation within the gauge framework.)

Русский

Если x ∈ s⋅c и c ≠ 0, то x ∈ c·s.

LaTeX

$$$x \in c \cdot s \Rightarrow x \in c \cdot s$$$

Lean4

/-- If `c • x ∈ s` and `c ≠ 0`, then `egauge 𝕜 s x` is at most `(‖c‖₊⁻¹ : ℝ≥0)`.

See also `egauge_le_of_smul_mem`. -/
theorem egauge_le_of_smul_mem_of_ne (h : c • x ∈ s) (hc : c ≠ 0) : egauge 𝕜 s x ≤ (‖c‖₊⁻¹ : ℝ≥0) :=
  by
  rw [← nnnorm_inv]
  exact egauge_le_of_mem_smul <| (mem_inv_smul_set_iff₀ hc _ _).2 h

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