inf' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem inf' (hf : Continuous f) (hg : Continuous g) : Continuous (f ⊓ g) :=
  hf.inf hg

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