term_⟂ₘ_ — Mathlib

English

If there exist sets s,t with μ(s) = 0, ν(t) = 0 and univ ⊆ s ∪ t, then μ ⟂ₘ ν.

Русский

Если существуют множества s,t такие, что μ(s) = 0, ν(t) = 0 и univ ⊆ s ∪ t, то μ ⟂ₘ ν.

LaTeX

$$$\mu(s) = 0 \rightarrow \nu(t) = 0 \rightarrow \mathrm{univ} \subseteq s \cup t \rightarrow \mu \perp_m \nu$$$

Lean4

@[inherit_doc MeasureTheory.Measure.MutuallySingular, scoped term_parser 1000]
public meta def «term_⟂ₘ_» : Lean.TrailingParserDescr✝ :=
  ParserDescr.trailingNode✝ `MeasureTheory.«term_⟂ₘ_» 60 60
    (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " ⟂ₘ ") (ParserDescr.cat✝ `term 61))

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