ae_ae_of_ae_comp — Mathlib

English

If ∀ᵐ z ∂(η ∘ κ) a, p z holds, then ∀ᵐ y ∂ κ a, ∀ᵐ z ∂ η y, p z.

Русский

Если верно для μ-почти всех z, что p z, то верно для κ a-почти всех y, и для η y-почти всех z, что p z.

LaTeX

$$$\\forall^{\\mathrm{ae}} z \\partial (\\eta \\circ_k \\kappa) a,\\; p z \\Rightarrow \\forall^{\\mathrm{ae}} y \\partial \\kappa a,\\; \\forall^{\\mathrm{ae}} z \\partial \\eta y,\\; p z.$$$

Lean4

theorem ae_ae_of_ae_comp (h : ∀ᵐ z ∂(η ∘ₖ κ) a, p z) : ∀ᵐ y ∂κ a, ∀ᵐ z ∂η y, p z :=
  ae_null_of_comp_null h

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