instSetLike — Mathlib

English

Extensionality principle for ProperCone: equality is determined by membership of all vectors.

Русский

Принцип экстенсиональности для ProperCone: равенство определяется членством всех векторов.

LaTeX

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

Lean4

instance : SetLike (ProperCone R E) E where
  coe C := C.carrier
  coe_injective' _ _ h := ProperCone.toPointedCone_injective <| SetLike.coe_injective h

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