adjoin_le_iff — Mathlib

English

The operation adjoin is monotone in its set argument: if s ⊆ t then adjoin(R,s) ≤ adjoin(R,t).

Русский

Операция порождения звёздной подалгебры монотонна по аргументу: если s ⊆ t, то adjoin(R,s) ≤ adjoin(R,t).

LaTeX

$$$s \subseteq t \Rightarrow \mathrm{adjoin}(R,s) \le \mathrm{adjoin}(R,t)$$$

Lean4

@[simp]
theorem adjoin_le_iff {S : StarSubalgebra R A} {s : Set A} : adjoin R s ≤ S ↔ s ⊆ S :=
  StarAlgebra.gc _ _

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