all_ae_of — Mathlib

English

If hp: ∀ᵐ a, ∀ i, p(a,i) holds, then for every i, ∀ᵐ a, p(a,i) holds.

Русский

Если hp: почти повсеместно ∀ i, p(a,i) выполняется, тогда для каждого i, почти повсеместно p(a,i) выполняется.

LaTeX

$$From hp: ∀ᵐ a, ∀ i, p(a,i), deduce ∀ i, ∀ᵐ a, p(a,i).$$

Lean4

theorem all_ae_of {ι : Sort*} {p : α → ι → Prop} (hp : ∀ᵐ a ∂μ, ∀ i, p a i) (i : ι) : ∀ᵐ a ∂μ, p a i := by
  filter_upwards [hp] with a ha using ha i

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