termMeasure[_]_ — Mathlib

English

If μ({a}) = 0 and μ({b}) = 0, then Ioo(a,b) =ᵐ μ Icc(a,b).

Русский

Если μ({a}) = 0 и μ({b}) = 0, то Ioo(a,b) =ᵐ μ Icc(a,b).

LaTeX

$$Ioo_ae_eq_Icc' (ha : μ { a } = 0) (hb : μ { b } = 0) : Ioo a b =ᵐ[μ] Icc a b$$

Lean4

/-- Notation for `Measure` with respect to a non-standard σ-algebra in the domain. -/
@[scoped term_parser 1000]
public meta def «termMeasure[_]_» : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `MeasureTheory.«termMeasure[_]_» 1022
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "Measure[") (ParserDescr.cat✝ `term 0))
        (ParserDescr.symbol✝ "] "))
      (ParserDescr.cat✝ `term 1023))

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