le_topologicalClosure — Mathlib

English

Let s be a subfield of a topological field α. Then s is contained in its topological closure: s ⊆ s.topologicalClosure.

Русский

Пусть s — подполе топологического поля α. Тогда s содержится в своем топологическом замыкании: s ⊆ s.topologicalClosure.

LaTeX

$$$s \subseteq s.topologicalClosure$$$

Lean4

theorem le_topologicalClosure (s : Subfield α) : s ≤ s.topologicalClosure :=
  _root_.subset_closure

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