inf' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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