upcrossingsBefore_bot — Mathlib

English

For any a,b and f, the value of upcrossingsBefore at the bottom of the order equals zero: upcrossingsBefore a b f ⊥ = ⊥.

Русский

Для любого a,b и f значение upcrossingsBefore в нулевом элементе порядка равно нулю: upcrossingsBefore a b f ⊥ = ⊥.

LaTeX

$$$\\mathrm{upcrossingsBefore}(a,b,f,\\bot,\\omega)=\\bot.$$$

Lean4

@[simp]
theorem upcrossingsBefore_bot [Preorder ι] [OrderBot ι] [InfSet ι] {a b : ℝ} {f : ι → Ω → ℝ} {ω : Ω} :
    upcrossingsBefore a b f ⊥ ω = ⊥ := by simp [upcrossingsBefore]

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