or — Mathlib · SciLib

English

If p and q are measurable predicates on α, then the disjunction p ∨ q is measurable.

Русский

Если p и q — измеримые предикаты на α, то их дизъюнкция p ∨ q измерима.

LaTeX

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

Lean4

theorem or (hp : Measurable p) (hq : Measurable q) : Measurable fun a ↦ p a ∨ q a :=
  measurableSet_setOf.1 <| hp.setOf.union hq.setOf

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