iff — Mathlib

English

If p and q are measurable predicates on α, then the equivalence p ↔ q is a measurable predicate.

Русский

Если p и q — измеримые предикаты, то эквивалентность p ↔ q измерима.

LaTeX

$$$\mathrm{Measurable}(p) \land \mathrm{Measurable}(q) \Rightarrow \mathrm{Measurable}(\lambda a. p(a) \leftrightarrow q(a))$$$

Lean4

theorem iff (hp : Measurable p) (hq : Measurable q) : Measurable fun a ↦ p a ↔ q a :=
  measurableSet_setOf.1 <| by simp_rw [iff_iff_implies_and_implies]; exact hq.setOf.bihimp hp.setOf

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