mem_closure — Mathlib

English

Membership in a convex cone's closure equals membership in the closure of its coercion.

Русский

Членство в замыкании выпуклого конуса эквивалентно членству в замыкании преобразованного множества.

LaTeX

$$a ∈ K.closure ↔ a ∈ closure (K : Set E)$$

Lean4

@[simp]
protected theorem mem_closure {K : ConvexCone 𝕜 E} {a : E} : a ∈ K.closure ↔ a ∈ closure (K : Set E) :=
  Iff.rfl

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