coe_mk — Mathlib

English

The canonical constructor mk of a compact set with a proof of compactness yields the set whose image is the given set.

Русский

Канонический конструктор mk компакта с доказательством компактности порождает множество, соответствующее данному множеству.

LaTeX

$$$\text{@[simp]}\ (mk\ s\ h) : Set\ alpha = s.$$$

Lean4

@[simp]
theorem coe_mk (s : Set α) (h) : (mk s h : Set α) = s :=
  rfl

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