inf — Mathlib

English

The infimum (pointwise) of two strongly measurable functions is strongly measurable in a normed setting with a continuous infimum operation.

Русский

Пусть f,g — сильно измеримые, тогда их точечный инфimum f ⊓ g тоже сильно измерим.

LaTeX

$$$\forall f,g:\alpha \to β, \text{StronglyMeasurable } f \land \text{StronglyMeasurable } g \Rightarrow \text{StronglyMeasurable } (x \mapsto f(x) \wedge g(x))$$$

Lean4

@[fun_prop, aesop safe 20 (rule_sets := [Measurable])]
protected theorem inf [Min β] [ContinuousInf β] (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) :
    StronglyMeasurable (f ⊓ g) :=
  ⟨fun n => hf.approx n ⊓ hg.approx n, fun x => (hf.tendsto_approx x).inf_nhds (hg.tendsto_approx x)⟩

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