stieltjesFunctionAux_def — Mathlib

English

The same auxiliary function can be described as the infimum over rationals r of the form r such that t < r, of f a r.

Русский

Аналогичное определение вспомогательной функции через инфимум по рациональным r с t < r.

LaTeX

$$$$\\mathrm{IsMeasurableRatCDF.stieltjesFunctionAux} f a = \\;\\; (t \\mapsto \\inf_{r : \\mathbb{Q}, t < r} f a r).$$$$

Lean4

theorem stieltjesFunctionAux_def : eta_helper Eq✝ @IsMeasurableRatCDF.stieltjesFunctionAux.{} @(delta% @definition✝) :=
  by
  intros
  delta IsMeasurableRatCDF.stieltjesFunctionAux
  rw [show wrapped✝ = ⟨@definition✝.{}, rfl✝⟩ from Subtype.ext✝ wrapped✝.2.symm✝]
  rfl

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