iInf_IicSnd_gt — Mathlib

English

Infimum over rationals r' > t of IicSnd r' applied to s equals IicSnd t applied to s.

Русский

Наименьшее по отношению к рациональным r' > t значение IicSnd r' на s равно IicSnd t на s.

LaTeX

$$$\bigwedge_{r' : \{ r' : \mathbb{Q} \mid t < r' \}} ρ.IicSnd(r')(s) = ρ.IicSnd(t)(s)$$$

Lean4

theorem iInf_IicSnd_gt (t : ℚ) {s : Set α} (hs : MeasurableSet s) [IsFiniteMeasure ρ] :
    ⨅ r : { r' : ℚ // t < r' }, ρ.IicSnd r s = ρ.IicSnd t s := by
  simp_rw [ρ.IicSnd_apply _ hs, Measure.iInf_rat_gt_prod_Iic hs]

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