coe_inj

Mathlib.Topology.Sets.Opens

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

English

The coercion map from Opens α to Set α is injective; equivalently, (↑U) = (↑V) iff U = V.

Русский

Коэрция из Opens α в Set α иньекция; то есть (↑U) = (↑V) эквивалентно U = V.

LaTeX

$$$(\uparrow U = \uparrow V) \iff U = V$.$$

Lean4

theorem coe_inj {U V : Opens α} : (U : Set α) = V ↔ U = V :=
  SetLike.ext'_iff.symm

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

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

Разделы

Аффилиация

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