closure_toSubmodule_eq

Mathlib.Topology.Algebra.Module.ClosedSubmodule

URI: https://scilib.ai/kg/mathlib#ClosedSubmodule.closure_toSubmodule_eq

← MathLib Explorer

English

For any Submodule s and ClosedSubmodule t, x ∈ closure(s) ⇔ x ∈ topologicalClosure(s).

Русский

Для подмодуля s и замкнутого t: x ∈ closure(s) ⇔ x ∈ topologicalClosure(s).

LaTeX

$$$x \in s.closure \iff x \in s.topologicalClosure$$$

Lean4

@[simp]
theorem closure_toSubmodule_eq {s : ClosedSubmodule R N} : s.toSubmodule.closure = s :=
  by
  ext x
  simp [closure_eq_iff_isClosed.mpr (ClosedSubmodule.isClosed s)]

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

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

Разделы

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

Аффилиация

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