mem_smul_of_zero_mem — Mathlib

English

The difference of two strictly convex sets is strictly convex.

Русский

Разность двух строго выпуклых множеств является строго выпуклым множеством.

LaTeX

$$$\StrictConvex 𝕜 s \rightarrow \StrictConvex 𝕜 t \rightarrow \StrictConvex 𝕜 (s - t)$$$

Lean4

theorem mem_smul_of_zero_mem (hs : StrictConvex 𝕜 s) (zero_mem : (0 : E) ∈ s) (hx : x ∈ s) (hx₀ : x ≠ 0) {t : 𝕜}
    (ht : 1 < t) : x ∈ t • interior s :=
  by
  rw [mem_smul_set_iff_inv_smul_mem₀ (by positivity)]
  exact hs.smul_mem_of_zero_mem zero_mem hx hx₀ (by positivity) (inv_lt_one_of_one_lt₀ ht)

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