superset — Mathlib

English

If φ ≤ ψ pointwise and ψ is measurable, then φ also forms an AECover with respect to the same μ and l.

Русский

Если φ(i) ⊆ ψ(i) по каждой точке и ψ измеримо, то φ тоже образует AECover относительно той же μ и l.

LaTeX

$$$\\text{AECover } μ l φ \\to \\text{AECover } μ l ψ$ provided $φ(i) \\subseteq ψ(i)$ and ψ is measurable.$$

Lean4

theorem superset {φ ψ : ι → Set α} (hφ : AECover μ l φ) (hsub : ∀ i, φ i ⊆ ψ i) (hmeas : ∀ i, MeasurableSet (ψ i)) :
    AECover μ l ψ :=
  ⟨hφ.1.mono fun _x hx ↦ hx.mono fun i hi ↦ hsub i hi, hmeas⟩

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