map_mono

Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic

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

English

If s1 is contained in s2, then the images satisfy s1.map f ≤ s2.map f.

Русский

Если s1 ⊆ s2, то их образы под отображением f удовлетворяют s1.map f ⊆ s2.map f.

LaTeX

$$$ s_1 \\le s_2 \\Rightarrow s_1.map f \\le s_2.map f$$$

Lean4

@[gcongr]
theorem map_mono {s₁ s₂ : AffineSubspace k P₁} (h : s₁ ≤ s₂) : s₁.map f ≤ s₂.map f :=
  Set.image_mono h

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

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

Разделы

Аффилиация

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