coe_mk

Mathlib.Topology.Sets.Order

URI: https://scilib.ai/kg/mathlib#ClopenUpperSet.coe_mk

English

The coercion of the constructor mk returns the original set.

Русский

Коэрцирование конструктора mk возвращает исходное множество.

LaTeX

$$$\\\\operatorname{coe\\\\_mk}(s, h) : (mk\\\\ s h : Set\\\\alpha) = s \\\\Rightarrow \\\\text{rfl}$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru