himp — Mathlib

English

If S1 and S2 are measurable subsets of α, then the set of points where S1 implies S2 is measurable. Equivalently, S1ᶜ ∪ S2 is measurable.

Русский

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

LaTeX

$$$\mathrm{MeasurableSet}(s_1) \rightarrow \mathrm{MeasurableSet}(s_2) \rightarrow \mathrm{MeasurableSet}(s_1^{\complement} \cup s_2)$$$

Lean4

@[simp, measurability]
protected theorem himp {s₁ s₂ : Set α} (h₁ : MeasurableSet s₁) (h₂ : MeasurableSet s₂) : MeasurableSet (s₁ ⇨ s₂) := by
  rw [himp_eq]; exact h₂.union h₁.compl

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