inf — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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