smul_mem_iff_mem — Mathlib

English

For any nonzero scalar c, x ∈ fundamentalCone(K) iff c·x ∈ fundamentalCone(K).

Русский

Для ненулевого скаляра c верно: x в фундаментальном конусе эквивалентно c·x в фундаментальном конусе.

LaTeX

$$(c ≠ 0) \Rightarrow (c\cdot x \in fundamentalCone(K) \iff x \in fundamentalCone(K)).$$

Lean4

theorem smul_mem_iff_mem (hc : c ≠ 0) : c • x ∈ fundamentalCone K ↔ x ∈ fundamentalCone K :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ smul_mem_of_mem h hc⟩
  convert smul_mem_of_mem h (inv_ne_zero hc)
  rw [eq_inv_smul_iff₀ hc]

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