adjoin_mono

Mathlib.Algebra.Star.NonUnitalSubalgebra

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

English

Monotonicity of adjoin with respect to set inclusion (repetition).

Русский

Повторное утверждение монотонности adjoin по включению множеств.

LaTeX

$$$$ s \\subseteq t \\Rightarrow \\\\operatorname{adjoin}_R(s) \\\\le \\\\operatorname{adjoin}_R(t) $$$$

Lean4

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

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

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

Разделы

Аффилиация

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