leastGE_mono

Mathlib.Probability.Martingale.BorelCantelli

URI: https://scilib.ai/kg/mathlib#MeasureTheory.leastGE_mono

English

If n ≤ m, then leastGE f r n ω ≤ leastGE f r m ω for all ω.

Русский

Если n ≤ m, то для всех ω выполняется leastGE f r n ω ≤ leastGE f r m ω.

LaTeX

$$∀ ω, instLENat.le (leastGE f r n ω) (leastGE f r m ω).$$

Lean4

theorem leastGE_mono {n m : ℕ} (hnm : n ≤ m) (r : ℝ) (ω : Ω) : leastGE f r n ω ≤ leastGE f r m ω :=
  hitting_mono hnm

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

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

Разделы

Аффилиация

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