pi_mono

Mathlib.Algebra.Algebra.Subalgebra.Pi

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

English

If for every i in s, t1(i) ≤ t2(i), then π(s,t1) ≤ π(s,t2).

Русский

Если для каждого i ∈ s выполняется t1(i) ≤ t2(i), то π(s,t1) ≤ π(s,t2).

LaTeX

$$($\forall i\in s,\ t_1(i) \le t_2(i)) \Rightarrow \pi(s,t_1) \le \pi(s,t_2)$$$

Lean4

@[gcongr]
theorem pi_mono (h : ∀ i ∈ s, t₁ i ≤ t₂ i) : pi s t₁ ≤ pi s t₂ :=
  Set.pi_mono h

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

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

Разделы

Аффилиация

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