ae_comp_of_ae_ae — Mathlib

English

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

Русский

Если ∀ᵐ z ∂ (η ∘ κ) a, p z, тогда ∀ᵐ y ∂ κ a, ∀ᵐ z ∂ η y, 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_comp_of_ae_ae (hp : MeasurableSet {z | p z}) (h : ∀ᵐ y ∂κ a, ∀ᵐ z ∂η y, p z) : ∀ᵐ z ∂(η ∘ₖ κ) a, p z :=
  by
  rwa [ae_iff, comp_null] at *
  exact hp.compl

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