English
The order relation on outer measures in relation to pi corresponds to a pointwise comparison over all product rectangles.
Русский
Порядок по отношению к pi для внешних мер эквивалентен покомпонентному сравнению по каждому прямоугольнику.
LaTeX
$$n \le \pi m \iff \forall s, \text{Nonempty}(\pi univ s) \Rightarrow n(\pi univ s) ≤ ∏_i m_i(s_i)$$
Lean4
theorem le_pi {m : ∀ i, OuterMeasure (α i)} {n : OuterMeasure (∀ i, α i)} :
n ≤ OuterMeasure.pi m ↔ ∀ s : ∀ i, Set (α i), (pi univ s).Nonempty → n (pi univ s) ≤ ∏ i, m i (s i) :=
by
rw [OuterMeasure.pi, le_boundedBy']; constructor
· intro h s hs; refine (h _ hs).trans_eq (piPremeasure_pi hs)
· intro h s hs; refine le_trans (n.mono <| subset_pi_eval_image univ s) (h _ ?_)
simp [univ_pi_nonempty_iff, hs]
