instNoAtoms_snd — Mathlib

English

If ν has no atoms, then μ × ν has no atoms.

Русский

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

LaTeX

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

Lean4

instance instNoAtoms_snd [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

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