mem_toCone' — Mathlib

English

Let hs be convex and s a subset. Then x ∈ hs.toCone s if and only if there exists a positive scalar c with c · x ∈ s.

Русский

Пусть hs выпукло и s — подмножество. Тогда x ∈ hs.toCone s эквивалентно существованию положительного числа c such that c·x ∈ s.

LaTeX

$$$ x \in hs.toCone s \iff \exists c \; (0 < c) \wedge c \cdot x \in s $$$

Lean4

theorem mem_toCone' : x ∈ hs.toCone s ↔ ∃ c : 𝕜, 0 < c ∧ c • x ∈ s :=
  by
  refine hs.mem_toCone.trans ⟨?_, ?_⟩
  · rintro ⟨c, hc, y, hy, rfl⟩
    exact ⟨c⁻¹, inv_pos.2 hc, by rwa [smul_smul, inv_mul_cancel₀ hc.ne', one_smul]⟩
  · rintro ⟨c, hc, hcx⟩
    exact ⟨c⁻¹, inv_pos.2 hc, _, hcx, by rw [smul_smul, inv_mul_cancel₀ hc.ne', one_smul]⟩

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