iInf_Prop — Mathlib

English

Analogous to iSup over a proposition, the infimum over a proposition is measurable if the base is measurable.

Русский

Аналогично iSup: инфимум по пропозиции измерим, если база измерима.

LaTeX

$$∀ p, ∀ f, (Measurable f) → Measurable fun b => iInf _ : p, f b$$

Lean4

@[measurability, fun_prop]
theorem iInf_Prop {α} {mα : MeasurableSpace α} [ConditionallyCompleteLattice α] (p : Prop) {f : δ → α}
    (hf : Measurable f) : Measurable fun b => ⨅ _ : p, f b := by
  classical
  simp_rw [ciInf_eq_ite]
  split_ifs with h
  · exact hf
  · exact measurable_const

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