term_≪_ — Mathlib

English

If μ ≪ ν, then c • μ ≪ c • ν for any c in R, with appropriate scalar structure.

Русский

Если μ ≪ ν, то для любого скалярного множителя c верно c • μ ≪ c • ν, при условии наличия соответствующей структуры скаляра.

LaTeX

$$$\mu \ll \nu \rightarrow (c \cdot \mu) \ll (c \cdot \nu)$$$

Lean4

@[inherit_doc MeasureTheory.Measure.AbsolutelyContinuous, scoped term_parser 1000]
public meta def «term_≪_» : Lean.TrailingParserDescr✝ :=
  ParserDescr.trailingNode✝ `MeasureTheory.«term_≪_» 50 50
    (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " ≪ ") (ParserDescr.cat✝ `term 51))

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