bihimp — Mathlib

English

If S1 and S2 are measurable subsets of α, then the biconditional S1 ⇔ S2 (the set of x with x ∈ S1 ⇔ x ∈ S2) is measurable.

Русский

Если A и B — измеримые подмножества α, то множество {x : x ∈ A ⇔ x ∈ B} измеримо.

LaTeX

$$$\mathrm{MeasurableSet}(s_1) \rightarrow \mathrm{MeasurableSet}(s_2) \rightarrow \mathrm{MeasurableSet}(s_1 \Leftrightarrow s_2)$$$

Lean4

@[simp, measurability]
protected theorem bihimp {s₁ s₂ : Set α} (h₁ : MeasurableSet s₁) (h₂ : MeasurableSet s₂) : MeasurableSet (s₁ ⇔ s₂) :=
  (h₂.himp h₁).inter (h₁.himp h₂)

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