pi_mono

Mathlib.LinearAlgebra.Pi

URI: https://scilib.ai/kg/mathlib#Submodule.pi_mono

English

If p_i ≤ q_i for all i ∈ I, then the pi I p is contained in pi I q.

Русский

Если для всех i ∈ I выполняется p_i ≤ q_i, то pi I p ≤ pi I q.

LaTeX

$$$$\\big( \\forall i\\in I,\\ p_i \\le q_i \\big) \\Rightarrow \\pi I p \\le \\pi I q.$$$$

Lean4

@[gcongr]
theorem pi_mono {s : Set ι} (h : ∀ i ∈ s, p i ≤ q i) : pi s p ≤ pi s q :=
  Set.pi_mono h

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

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

Разделы

Аффилиация

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