of_nonempty_of_isClosed — Mathlib

English

If a nonempty closed convex cone K in a space E has the stated closure properties, then K is pointed.

Русский

Если выпуклый конус K ненулевой и замкнут, то он остроконечен.

LaTeX

$$ConvexCone.Pointed( K )$$

Lean4

theorem of_nonempty_of_isClosed (hC : (C : Set E).Nonempty) (hSclos : IsClosed (C : Set E)) : C.Pointed :=
  by
  obtain ⟨x, hx⟩ := hC
  let f : 𝕜 → E :=
    (· • x)
      -- The closure of `f (0, ∞)` is a subset of `C`

  have hfS : closure (f '' Set.Ioi 0) ⊆ C :=
    hSclos.closure_subset_iff.2 <| by rintro _ ⟨_, h, rfl⟩; exact C.smul_mem h hx
  have fc : ContinuousWithinAt f (Set.Ioi (0 : 𝕜)) 0 := (continuous_id.smul continuous_const).continuousWithinAt
  simpa [f, Pointed, ← SetLike.mem_coe] using hfS <| fc.mem_closure_image <| by simp

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