inf' — Mathlib

English

If f,g: X → L are ContinuousWithinAt s at x, then f ⊓ g is ContinuousWithinAt s at x.

Русский

Если f,g: X → L непрерывны внутри s в x, то f ⊓ g непрерывна внутри s в x.

LaTeX

$$$\\forall L X\\ [TopologicalSpace L]\\ [TopologicalSpace X]\\ [Min L]\\ [ContinuousInf L],\\ \\forall f,g:X \\to L,\\ \\forall s:\\!\\text{Set } X,\\ \\forall x:X,\\ ContinuousWithinAt f\\ s\\ x\\land\\ ContinuousWithinAt g\\ s\\ x\\Rightarrow ContinuousWithinAt\\ (\\lambda a \\mapsto f\\ a \\;\\inf\\; g\\ a)\\ s\\ x.$$$

Lean4

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

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