toPointedCone_injective — Mathlib

English

Two proper cones are equal if and only if they have the same membership relation for all vectors.

Русский

Два правильных конуса равны тогда, когда по каждому вектору совпадает множество их членов.

LaTeX

$$ext (h : ∀ x, x ∈ C1 ↔ x ∈ C2) : C1 = C2$$

Lean4

theorem toPointedCone_injective : Injective ((↑) : ProperCone R E → PointedCone R E) :=
  ClosedSubmodule.toSubmodule_injective

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