instNoAtoms_fst — Mathlib

English

If μ has no atoms, then the product measure μ × ν also has no atoms.

Русский

Если мера μ не имеет атомов, то и произведённая мера μ × ν не имеет атомов.

LaTeX

$$$\text{NoAtoms}(\mu) \Rightarrow \text{NoAtoms}(\mu \mathrm{.prod} ν)$$$

Lean4

instance instNoAtoms_fst [NoAtoms μ] : NoAtoms (Measure.prod μ ν) where
  measure_singleton
    | (x, y) =>
      nonpos_iff_eq_zero.mp <|
        calc
          μ.prod ν {(x, y)} = μ.prod ν ({ x } ×ˢ { y }) := by rw [singleton_prod_singleton]
          _ ≤ μ { x } * ν { y } := (prod_prod_le _ _)
          _ = 0 := by simp

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