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

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

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