inf' — Mathlib

English

If f,g : X → L are ContinuousAt x, then their pointwise infimum f ⊓ g is ContinuousAt x.

Русский

Если f,g: X → L непрерывны в точке x, то их поэлементный минимум f ⊓ g непрерывен в x.

LaTeX

$$$\\forall L X\\ [TopologicalSpace L]\\ [TopologicalSpace X]\\ [Min L]\\ [ContinuousInf L],\\ \\forall f,g:X \\to L,\\ \\forall x:X,\\ ContinuousAt\\ f\\ x\\land\\ ContinuousAt\\ g\\ x\\Rightarrow ContinuousAt\\ (\\lambda a \\mapsto f\\ a \\;\\inf\\; g\\ a)\\ x.$$$

Lean4

theorem inf' (hf : ContinuousAt f x) (hg : ContinuousAt g x) : ContinuousAt (f ⊓ g) x :=
  hf.inf_nhds' hg

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