topologicalClosure_minimal — Mathlib

English

If s ⊆ t and t is closed, then s.topologicalClosure ⊆ t; i.e., the closure of s is the smallest closed subfield containing s.

Русский

Если s ⊆ t и t замкнуто, то s.topologicalClosure ⊆ t; то есть замыкание s является наименьшим замкнутым подполем, содержащим s.

LaTeX

$$$s.topologicalClosure \subseteq t\quad\text{whenever } s \le t \text{ and } IsClosed\left( t : Set \alpha \right)$$$

Lean4

theorem topologicalClosure_minimal (s : Subfield α) {t : Subfield α} (h : s ≤ t) (ht : IsClosed (t : Set α)) :
    s.topologicalClosure ≤ t :=
  closure_minimal h ht

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