ext — Mathlib

English

Two convex cones are equal if and only if they have the same elements.

Русский

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

LaTeX

$$$\\forall x, x \\in C_1 \\iff x \\in C_2 \\Rightarrow C_1 = C_2$$$

Lean4

/-- Two `ConvexCone`s are equal if they have the same elements. -/
@[ext]
theorem ext (h : ∀ x, x ∈ C₁ ↔ x ∈ C₂) : C₁ = C₂ :=
  SetLike.ext h

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