star_mono

Mathlib.Algebra.Star.Subalgebra

URI: https://scilib.ai/kg/mathlib#Subalgebra.star_mono

English

The star operation on subalgebras is monotone: if S ≤ T then star(S) ≤ star(T).

Русский

Операция взятия звезды над подалгебрами монотонна: если S меньше T, то star(S) меньше или равно star(T).

LaTeX

$$$$S \le T \implies \mathrm{star}(S) \le \mathrm{star}(T).$$$$

Lean4

theorem star_mono : Monotone (star : Subalgebra R A → Subalgebra R A) := fun _ _ h _ hx => h hx

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

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

Разделы

Аффилиация

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