adjoin_mono

Mathlib.Algebra.Star.Subalgebra

URI: https://scilib.ai/kg/mathlib#StarAlgebra.adjoin_mono

English

Same monotonicity statement: 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

@[gcongr]
theorem adjoin_mono {s t : Set A} (H : s ⊆ t) : adjoin R s ≤ adjoin R t :=
  StarAlgebra.gc.monotone_l H

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru