map₂_le_map₂_left

Mathlib.Algebra.Module.Submodule.Bilinear

URI: https://scilib.ai/kg/mathlib#Submodule.map₂_le_map₂_left

← MathLib Explorer

English

If p1 ≤ p2 then map₂ f p1 q ≤ map₂ f p2 q.

Русский

Если p1 ≤ p2, то map₂ f p1 q ≤ map₂ f p2 q.

LaTeX

$$p_1 \\le p_2 \\Rightarrow map_2 f p_1 q \\le map_2 f p_2 q$$

Lean4

theorem map₂_le_map₂_left {f : M →ₗ[R] N →ₗ[R] P} {p₁ p₂ : Submodule R M} {q : Submodule R N} (h : p₁ ≤ p₂) :
    map₂ f p₁ q ≤ map₂ f p₂ q :=
  map₂_le_map₂ h (le_refl q)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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