inter — Mathlib

English

The elementwise intersection of two AECovers is again an AECover.

Русский

Построение поэлементного пересечения двух AECoverAgain образует AECover.

LaTeX

$$$\\text{AECover } μ l φ \\cap ψ$ = AECover $μ l (i \\mapsto φ(i) \\cap ψ(i))$$$

Lean4

/-- Elementwise intersection of two `AECover`s is an `AECover`. -/
theorem inter {φ ψ : ι → Set α} (hφ : AECover μ l φ) (hψ : AECover μ l ψ) : AECover μ l (fun i ↦ φ i ∩ ψ i)
    where
  ae_eventually_mem := hψ.1.mp <| hφ.1.mono fun _ ↦ Eventually.and
  measurableSet _ := (hφ.2 _).inter (hψ.2 _)

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