mem_smul — Mathlib

English

If s is star-convex at 0 and x∈s, then for t≥1, t x ∈ t s.

Русский

Если s звёздочно выпукло относительно 0 и x ∈ s, то t x ∈ t s при t ≥ 1.

LaTeX

$$$\\text{StarConvex}_{\\mathbb{K}}(0,s) \\wedge x\\in s \\Rightarrow \\forall t\\ge 1:\\ t\\cdot x \\in t\\cdot s$$$

Lean4

theorem mem_smul (hs : StarConvex 𝕜 0 s) (hx : x ∈ s) {t : 𝕜} (ht : 1 ≤ t) : x ∈ t • s :=
  by
  rw [mem_smul_set_iff_inv_smul_mem₀ (zero_lt_one.trans_le ht).ne']
  exact hs.smul_mem hx (by positivity) (inv_le_one_of_one_le₀ ht)

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