isClosed — Mathlib

English

For any x ∈ A, the underlying set of elemental R x is closed in A; i.e., the set of elements of the elemental subalgebra is a closed subset of A.

Русский

Для любого x ∈ A множество элементов элементарной подалгебры является замкнутым подмножеством A.

LaTeX

$$IsClosed ((elemental R x) : Set A)$$

Lean4

instance isClosed (x : A) : IsClosed (elemental R x : Set A) :=
  isClosed_topologicalClosure _

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