le_of_mem — Mathlib

English

The elements of the topological closure of the elemental algebra form a commutative nonunital ring.

Русский

Элементы топологического замыкания элементарной алгебры образуют коммутативное немодульное кольцо без единицы.

LaTeX

$$NonUnitalCommRing (Subtype (mem (elemental R x) .topologicalClosure))$$

Lean4

theorem le_of_mem {x : A} {s : NonUnitalSubalgebra R A} (hs : IsClosed (s : Set A)) (hx : x ∈ s) : elemental R x ≤ s :=
  topologicalClosure_minimal (adjoin_le <| by simpa using hx) hs

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