smul_mem_iff — Mathlib

English

Let C be a convex cone in a module M over a field 𝕜 with 𝕜 a linearly ordered field. For any c > 0, c · x ∈ C if and only if x ∈ C for all x ∈ M.

Русский

Пусть C — выпуклый конус в модуле M над полем 𝕜, причём 𝕜 является линейно упорядоченным полем. Для любого c > 0 выполняется: c · x ∈ C тогда и только тогда, когда x ∈ C для всех x ∈ M.

LaTeX

$$$ (0 < c) \rightarrow (\forall x \in M,\ c \cdot x \in C \leftrightarrow x \in C). $$$

Lean4

theorem smul_mem_iff {c : 𝕜} (hc : 0 < c) {x : M} : c • x ∈ C ↔ x ∈ C :=
  ⟨fun h => inv_smul_smul₀ hc.ne' x ▸ C.smul_mem (inv_pos.2 hc) h, C.smul_mem hc⟩

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