sup_le — Mathlib

English

The coeFn_inf lemma states that the infimum (minimum) of two μ-ae equivalence classes is a.e. equal to the pointwise infimum of the representatives.

Русский

Лемма coeFn_inf утверждает, что инфимум ae-классов равен по мере почти везде инфимуму представлений.

LaTeX

$$$(f \inf g).cast a =^\mathrm{ae}_{μ} f.cast a \inf g.cast a$ for all a.$$

Lean4

protected theorem sup_le (f g f' : α →ₘ[μ] β) (hf : f ≤ f') (hg : g ≤ f') : f ⊔ g ≤ f' :=
  by
  rw [← coeFn_le] at hf hg ⊢
  filter_upwards [hf, hg, coeFn_sup f g] with _ haf hag ha_sup
  rw [ha_sup]
  exact sup_le haf hag

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