mem_adjoin_of_mem — Mathlib

English

The equality adjoin R s = (Algebra.adjoin R s).starClosure holds, expressing the universal property of star-closure with respect to adjoin.

Русский

Равенство adjoin R s = (Algebra.adjoin R s).starClosure выражает универсальное свойство звёздного замыкания относительно adjoin.

LaTeX

$$$\mathrm{adjoin}(R,s) = (\mathrm{Algebra.adjoin}(R,s)).\mathrm{starClosure}.$$$

Lean4

@[aesop 80% (rule_sets := [SetLike])]
theorem mem_adjoin_of_mem {s : Set A} {x : A} (hx : x ∈ s) : x ∈ adjoin R s :=
  subset_adjoin R s hx

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