inter_pos_of_cond_ne_zero — Mathlib

English

If S is measurable and μ(T | S) ≠ 0, then μ(S ∩ T) > 0.

Русский

Если S измеримо и μ(T | S) ≠ 0, то μ(S ∩ T) > 0.

LaTeX

$$$\\text{MeasurableSet}(S) \\;\\land\\; μ(T|S) \\neq 0 \\quad\\Rightarrow\\quad 0 < μ(S \\cap T)$$$

Lean4

theorem inter_pos_of_cond_ne_zero (hms : MeasurableSet s) (hcst : μ[t | s] ≠ 0) : 0 < μ (s ∩ t) :=
  by
  refine pos_iff_ne_zero.mpr (right_ne_zero_of_mul (a := (μ s)⁻¹) ?_)
  convert hcst
  simp [hms, Set.inter_comm, cond]

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