inf — Mathlib

English

If f,g: X → L are continuous and L is a topological lattice with continuous inf, then x ↦ f(x) ⊓ g(x) is continuous.

Русский

Пусть f,g: X → L непрерывны; если в L непрерывна операция инфимум, то x ↦ f(x) ⊓ g(x) непрерывна.

LaTeX

$$$(\\text{hf} : \\text{Continuous}(f)) \\land (\\text{hg} : \\text{Continuous}(g)) \\Rightarrow \\text{Continuous}(x \\mapsto f(x) \\wedge g(x))$$$

Lean4

@[continuity, fun_prop]
theorem inf [Min L] [ContinuousInf L] {f g : X → L} (hf : Continuous f) (hg : Continuous g) :
    Continuous fun x => f x ⊓ g x :=
  continuous_inf.comp (hf.prodMk hg :)

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