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⟩