exists_upperCrossingTime_eq — Mathlib

English

There exists n such that upperCrossingTime(a,b,f,N,n,ω) = N, assuming a<b.

Русский

Существует n такое, что upperCrossingTime(a,b,f,N,n,ω) = N при a < b.

LaTeX

$$$\forall f,N,ω\; (a < b) \Rightarrow \exists n\; upperCrossingTime(a,b,f,N,n,ω) = N$$$

Lean4

theorem exists_upperCrossingTime_eq (f : ℕ → Ω → ℝ) (N : ℕ) (ω : Ω) (hab : a < b) :
    ∃ n, upperCrossingTime a b f N n ω = N := by
  by_contra h; push_neg at h
  have : StrictMono fun n => upperCrossingTime a b f N n ω :=
    strictMono_nat_of_lt_succ fun n => upperCrossingTime_lt_succ hab (h _)
  obtain ⟨_, ⟨k, rfl⟩, hk⟩ : ∃ (m : _) (_ : m ∈ Set.range fun n => upperCrossingTime a b f N n ω), N < m :=
    ⟨upperCrossingTime a b f N (N + 1) ω, ⟨N + 1, rfl⟩, lt_of_lt_of_le N.lt_succ_self (StrictMono.id_le this (N + 1))⟩
  exact not_le.2 hk upperCrossingTime_le

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