coe_mk

Mathlib.Topology.Sets.Opens

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.Opens.coe_mk

← MathLib Explorer

English

The coercion from Opens α to Set α applied to the pair ⟨U,h⟩ equals U.

Русский

Коэрсия из Opens α в Set α применительно к паре ⟨U,h⟩ равна U.

LaTeX

$$$\uparrow(\langle U, h\rangle : Opens α) = U$.$$

Lean4

/-- the coercion `Opens α → Set α` applied to a pair is the same as taking the first component -/
@[simp]
theorem coe_mk {U : Set α} {hU : IsOpen U} : ↑(⟨U, hU⟩ : Opens α) = U :=
  rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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