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

@[fun_prop]
theorem inf (hf : ContinuousAt f x) (hg : ContinuousAt g x) : ContinuousAt (fun a ↦ f a ⊓ g a) x :=
  hf.inf' hg

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