carrier_eq_coe

Mathlib.Topology.Sets.Closeds

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.Closeds.carrier_eq_coe

English

The carrier of a closed set is equal to its underlying set when viewed as a subset of α.

Русский

Носитель замкнутого множества равен его базовому множеству при виде как подмножество α.

LaTeX

$$$s.\text{carrier} = (s : Set \alpha)$$$

Lean4

@[simp]
theorem carrier_eq_coe (s : Closeds α) : s.carrier = (s : Set α) :=
  rfl

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

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

Разделы

Аффилиация

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