map_mono

Mathlib.Algebra.Star.Subalgebra

URI: https://scilib.ai/kg/mathlib#StarSubalgebra.map_mono

English

If S1 ≤ S2, then S1.map f ≤ S2.map f.

Русский

Если S1 ≤ S2, то S1.map f ≤ S2.map f.

LaTeX

$$$S_1 \le S_2 \Rightarrow S_1.map f \le S_2.map f$$$

Lean4

theorem map_mono {S₁ S₂ : StarSubalgebra R A} {f : A →⋆ₐ[R] B} : S₁ ≤ S₂ → S₁.map f ≤ S₂.map f :=
  Set.image_mono

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

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

Разделы

Аффилиация

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