meas_countablePartitionSet_le_of_fst_le

English

For any hκν : fst κ ≤ ν, and partitions, the density on a subset is bounded by its density on a larger subset: κ a (countablePartitionSet n x ×ˢ s) ≤ ν a (countablePartitionSet n x).

Русский

Плотность на частицы разбиения не превосходит плотности на большем множестве: κ a(countablePartitionSet n x × s) ≤ ν a(countablePartitionSet n x).

LaTeX

$$$\kappa a\big(\text{countablePartitionSet } n x \times^s s\big) \le \nu a\big(\text{countablePartitionSet } n x\big)$$$

Lean4

theorem meas_countablePartitionSet_le_of_fst_le (hκν : fst κ ≤ ν) (n : ℕ) (a : α) (x : γ) (s : Set β) :
    κ a (countablePartitionSet n x ×ˢ s) ≤ ν a (countablePartitionSet n x) := by
  calc
    κ a (countablePartitionSet n x ×ˢ s) ≤ fst κ a (countablePartitionSet n x) :=
      by
      rw [fst_apply' _ _ (measurableSet_countablePartitionSet _ _)]
      refine measure_mono (fun x ↦ ?_)
      simp only [mem_prod, mem_setOf_eq, and_imp]
      exact fun h _ ↦ h
    _ ≤ ν a (countablePartitionSet n x) := hκν a _

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