lowerCrossingTime_zero — Mathlib

English

The base case for the lower crossing time is the hitting time from c to N of the set {x ≤ a}.

Русский

Базовый случай для нижнего времени пересечения — попадание из c до N в множество {x ≤ a}.

LaTeX

$$$ lowerCrossingTime(a,b,f,N,0) = hitting\\, f\\; (\\{x \\le a\\}) \\; \\operatorname{bot} \\; N $$$

Lean4

@[simp]
theorem lowerCrossingTime_zero : lowerCrossingTime a b f N 0 = hitting f (Set.Iic a) ⊥ N :=
  rfl

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