ae_comp_iff — Mathlib

English

If hp: MeasurableSet {z | p z}, then (∀ᵐ z ∂ (η ∘ κ) a, p z) ↔ ∀ᵐ y ∂ κ a, ∀ᵐ z ∂ η y, p z.

Русский

Если hp: разрешимо множество {z | p z}, тогда эквивалентно: ∀ᵐ z ∂ (η ∘ κ) a, p z ⇔ ∀ᵐ y ∂ κ a, ∀ᵐ z ∂ η y, p z.

LaTeX

$$$\\text{hp}:\\ MeasurableSet\\{z: p(z)\\} \\Rightarrow\\ (\\forall^{\\mathrm{ae}} z \\partial (\\eta \\circ_k \\kappa), p z) \\iff (\\forall^{\\mathrm{ae}} y \\partial \\kappa a, \\forall^{\\mathrm{ae}} z \\partial \\eta y, p z).$$$

Lean4

theorem ae_comp_iff (hp : MeasurableSet {z | p z}) : (∀ᵐ z ∂(η ∘ₖ κ) a, p z) ↔ ∀ᵐ y ∂κ a, ∀ᵐ z ∂η y, p z :=
  ⟨ae_ae_of_ae_comp, ae_comp_of_ae_ae hp⟩

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