pi_pi_le — Mathlib

English

For any m and any s, OuterMeasure.pi m (pi univ s) ≤ ∏ i m_i(s_i).

Русский

Для любых m и s верно неравенство OuterMeasure.pi m (pi univ s) ≤ ∏_i m_i(s_i).

LaTeX

$$\OuterMeasure.pi(m)(\pi univ s) ≤ ∏_i m_i(s_i)$$

Lean4

theorem pi_pi_le (m : ∀ i, OuterMeasure (α i)) (s : ∀ i, Set (α i)) : OuterMeasure.pi m (pi univ s) ≤ ∏ i, m i (s i) :=
  by
  rcases (pi univ s).eq_empty_or_nonempty with h | h
  · simp [h]
  exact (boundedBy_le _).trans_eq (piPremeasure_pi h)

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