instSetLike — Mathlib

English

ConvexCone is equipped with a SetLike structure, i.e., it can be viewed as a subset of M with equality determined by membership.

Русский

ConvexCone снабжен структурой SetLike, то есть он рассматривается как подмножество M, равенство определяется по принадлежности.

LaTeX

$$$\\text{ConvexCone}\\,R\\,M \\text{ has a SetLike structure with carrier in } M$$$

Lean4

instance : SetLike (ConvexCone R M) M where
  coe := carrier
  coe_injective' C₁ C₂ h := by cases C₁; congr!

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