and — Mathlib

English

If p and q are measurable predicates on α, then the conjunction 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) \land q(a))$$$

Lean4

theorem and (hp : Measurable p) (hq : Measurable q) : Measurable fun a ↦ p a ∧ q a :=
  measurableSet_setOf.1 <| hp.setOf.inter hq.setOf

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