ite' — Mathlib

English

For any proposition p, if s is MeasurableSet whenever p holds and t is MeasurableSet whenever p does not hold, then ite p s t is measurable.

Русский

Для произвольного p: если при выполнении p множество s измеримо, а при не выполнении p множество t измеримо, то ite p s t измеримо.

LaTeX

$$$\\forall p, (p \\rightarrow \\mathrm{MeasurableSet}(s)) \\rightarrow (\\lnot p \\rightarrow \\mathrm{MeasurableSet}(t)) \\rightarrow \\mathrm{MeasurableSet}(\\mathrm{ite}\ \\, p\ \\, s\ \\, t)$$$

Lean4

theorem ite' {s t : Set α} {p : Prop} (hs : p → MeasurableSet s) (ht : ¬p → MeasurableSet t) :
    MeasurableSet (ite p s t) := by
  split_ifs with h
  exacts [hs h, ht h]

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